Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnflem1cOLD Structured version   Unicode version

Theorem cantnflem1cOLD 8161
 Description: Lemma for cantnfOLD 8166. (Contributed by Mario Carneiro, 4-Jun-2015.) Obsolete version of cantnflem1a 8136 as of 2-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cantnfsOLD.1 CNF
cantnfsOLD.2
cantnfsOLD.3
oemapvalOLD.t
oemapvalOLD.3
oemapvalOLD.4
oemapvalOLD.5
oemapvalOLD.6
cantnflem1OLD.o OrdIso
Assertion
Ref Expression
cantnflem1cOLD
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,   ,,,,,   ,,,,,   ,,,,,,   ,,,,,   ,,,,   ,,,,,   ,   ,
Allowed substitution hints:   ()   ()   (,,,)   ()   ()

Proof of Theorem cantnflem1cOLD
StepHypRef Expression
1 simplr 754 . 2
2 cantnfsOLD.1 . . . . . . . 8 CNF
3 cantnfsOLD.2 . . . . . . . 8
4 cantnfsOLD.3 . . . . . . . 8
5 oemapvalOLD.t . . . . . . . 8
6 oemapvalOLD.3 . . . . . . . 8
7 oemapvalOLD.4 . . . . . . . 8
8 oemapvalOLD.5 . . . . . . . 8
9 oemapvalOLD.6 . . . . . . . 8
102, 3, 4, 5, 6, 7, 8, 9oemapvali 8135 . . . . . . 7
1110simp3d 1011 . . . . . 6
1211ad3antrrr 728 . . . . 5
13 cantnflem1OLD.o . . . . . . . 8 OrdIso
142, 3, 4, 5, 6, 7, 8, 9, 13cantnflem1bOLD 8160 . . . . . . 7
1514ad2antrr 724 . . . . . 6
16 simprr 758 . . . . . 6
1710simp1d 1009 . . . . . . . . 9
18 onelon 5435 . . . . . . . . 9
194, 17, 18syl2anc 659 . . . . . . . 8
2019ad3antrrr 728 . . . . . . 7
21 onss 6608 . . . . . . . . . . 11
224, 21syl 17 . . . . . . . . . 10
2322sselda 3442 . . . . . . . . 9
2423adantlr 713 . . . . . . . 8
2524adantr 463 . . . . . . 7
26 ontr2 5457 . . . . . . 7
2720, 25, 26syl2anc 659 . . . . . 6
2815, 16, 27mp2and 677 . . . . 5
29 eleq2 2475 . . . . . . 7
30 fveq2 5849 . . . . . . . 8
31 fveq2 5849 . . . . . . . 8
3230, 31eqeq12d 2424 . . . . . . 7
3329, 32imbi12d 318 . . . . . 6
3433rspcv 3156 . . . . 5
351, 12, 28, 34syl3c 60 . . . 4
36 simprl 756 . . . 4
3735, 36eqnetrrd 2697 . . 3
38 fvex 5859 . . . 4
39 dif1o 7187 . . . 4
4038, 39mpbiran 919 . . 3
4137, 40sylibr 212 . 2
422, 3, 4cantnfsOLD 8147 . . . . . . 7
437, 42mpbid 210 . . . . . 6
4443simpld 457 . . . . 5
45 ffn 5714 . . . . 5
4644, 45syl 17 . . . 4