Metamath Proof Explorer

Theorem soseq

Description: A linear ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011)

Ref Expression
Hypotheses soseq.1 ⊢ROrA∪∅
soseq.2 ⊢F=f|∃x∈Onf:x⟶A
soseq.3 ⊢S=fg|f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x
soseq.4 ⊢¬∅∈A
Assertion soseq ⊢SOrF

Proof

Step Hyp Ref Expression
1 soseq.1 ⊢ROrA∪∅
2 soseq.2 ⊢F=f|∃x∈Onf:x⟶A
3 soseq.3 ⊢S=fg|f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x
4 soseq.4 ⊢¬∅∈A
5 sopo ⊢ROrA∪∅→RPoA∪∅
6 1 5 ax-mp ⊢RPoA∪∅
7 6 2 3 poseq ⊢SPoF
8 eleq1w ⊢f=a→f∈F↔a∈F
9 8 anbi1d ⊢f=a→f∈F∧g∈F↔a∈F∧g∈F
10 fveq1 ⊢f=a→f⁡y=a⁡y
11 10 eqeq1d ⊢f=a→f⁡y=g⁡y↔a⁡y=g⁡y
12 11 ralbidv ⊢f=a→∀y∈xf⁡y=g⁡y↔∀y∈xa⁡y=g⁡y
13 fveq1 ⊢f=a→f⁡x=a⁡x
14 13 breq1d ⊢f=a→f⁡xRg⁡x↔a⁡xRg⁡x
15 12 14 anbi12d ⊢f=a→∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x
16 15 rexbidv ⊢f=a→∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃x∈On∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x
17 9 16 anbi12d ⊢f=a→f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔a∈F∧g∈F∧∃x∈On∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x
18 eleq1w ⊢g=b→g∈F↔b∈F
19 18 anbi2d ⊢g=b→a∈F∧g∈F↔a∈F∧b∈F
20 fveq1 ⊢g=b→g⁡y=b⁡y
21 20 eqeq2d ⊢g=b→a⁡y=g⁡y↔a⁡y=b⁡y
22 21 ralbidv ⊢g=b→∀y∈xa⁡y=g⁡y↔∀y∈xa⁡y=b⁡y
23 fveq1 ⊢g=b→g⁡x=b⁡x
24 23 breq2d ⊢g=b→a⁡xRg⁡x↔a⁡xRb⁡x
25 22 24 anbi12d ⊢g=b→∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x↔∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x
26 25 rexbidv ⊢g=b→∃x∈On∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x↔∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x
27 19 26 anbi12d ⊢g=b→a∈F∧g∈F∧∃x∈On∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x↔a∈F∧b∈F∧∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x
28 17 27 3 brabg ⊢a∈F∧b∈F→aSb↔a∈F∧b∈F∧∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x
29 28 bianabs ⊢a∈F∧b∈F→aSb↔∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x
30 eleq1w ⊢f=b→f∈F↔b∈F
31 30 anbi1d ⊢f=b→f∈F∧g∈F↔b∈F∧g∈F
32 fveq1 ⊢f=b→f⁡y=b⁡y
33 32 eqeq1d ⊢f=b→f⁡y=g⁡y↔b⁡y=g⁡y
34 33 ralbidv ⊢f=b→∀y∈xf⁡y=g⁡y↔∀y∈xb⁡y=g⁡y
35 fveq1 ⊢f=b→f⁡x=b⁡x
36 35 breq1d ⊢f=b→f⁡xRg⁡x↔b⁡xRg⁡x
37 34 36 anbi12d ⊢f=b→∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∀y∈xb⁡y=g⁡y∧b⁡xRg⁡x
38 37 rexbidv ⊢f=b→∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃x∈On∀y∈xb⁡y=g⁡y∧b⁡xRg⁡x
39 31 38 anbi12d ⊢f=b→f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔b∈F∧g∈F∧∃x∈On∀y∈xb⁡y=g⁡y∧b⁡xRg⁡x
40 eleq1w ⊢g=a→g∈F↔a∈F
41 40 anbi2d ⊢g=a→b∈F∧g∈F↔b∈F∧a∈F
42 fveq1 ⊢g=a→g⁡y=a⁡y
43 42 eqeq2d ⊢g=a→b⁡y=g⁡y↔b⁡y=a⁡y
44 43 ralbidv ⊢g=a→∀y∈xb⁡y=g⁡y↔∀y∈xb⁡y=a⁡y
45 fveq1 ⊢g=a→g⁡x=a⁡x
46 45 breq2d ⊢g=a→b⁡xRg⁡x↔b⁡xRa⁡x
47 44 46 anbi12d ⊢g=a→∀y∈xb⁡y=g⁡y∧b⁡xRg⁡x↔∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
48 47 rexbidv ⊢g=a→∃x∈On∀y∈xb⁡y=g⁡y∧b⁡xRg⁡x↔∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
49 41 48 anbi12d ⊢g=a→b∈F∧g∈F∧∃x∈On∀y∈xb⁡y=g⁡y∧b⁡xRg⁡x↔b∈F∧a∈F∧∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
50 39 49 3 brabg ⊢b∈F∧a∈F→bSa↔b∈F∧a∈F∧∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
51 50 bianabs ⊢b∈F∧a∈F→bSa↔∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
52 51 ancoms ⊢a∈F∧b∈F→bSa↔∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
53 29 52 orbi12d ⊢a∈F∧b∈F→aSb∨bSa↔∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
54 53 notbid ⊢a∈F∧b∈F→¬aSb∨bSa↔¬∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
55 ralinexa ⊢∀x∈On∀y∈xa⁡y=b⁡y→¬a⁡xRb⁡x∨b⁡xRa⁡x↔¬∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨b⁡xRa⁡x
56 andi ⊢∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨b⁡xRa⁡x↔∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∀y∈xa⁡y=b⁡y∧b⁡xRa⁡x
57 eqcom ⊢a⁡y=b⁡y↔b⁡y=a⁡y
58 57 ralbii ⊢∀y∈xa⁡y=b⁡y↔∀y∈xb⁡y=a⁡y
59 58 anbi1i ⊢∀y∈xa⁡y=b⁡y∧b⁡xRa⁡x↔∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
60 59 orbi2i ⊢∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∀y∈xa⁡y=b⁡y∧b⁡xRa⁡x↔∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
61 56 60 bitri ⊢∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨b⁡xRa⁡x↔∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
62 61 rexbii ⊢∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨b⁡xRa⁡x↔∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
63 r19.43 ⊢∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x↔∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
64 62 63 bitri ⊢∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨b⁡xRa⁡x↔∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
65 55 64 xchbinx ⊢∀x∈On∀y∈xa⁡y=b⁡y→¬a⁡xRb⁡x∨b⁡xRa⁡x↔¬∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x
66 feq2 ⊢x=y→f:x⟶A↔f:y⟶A
67 66 cbvrexvw ⊢∃x∈Onf:x⟶A↔∃y∈Onf:y⟶A
68 67 abbii ⊢f|∃x∈Onf:x⟶A=f|∃y∈Onf:y⟶A
69 2 68 eqtri ⊢F=f|∃y∈Onf:y⟶A
70 69 orderseqlem ⊢a∈F→a⁡x∈A∪∅
71 69 orderseqlem ⊢b∈F→b⁡x∈A∪∅
72 sotrieq ⊢ROrA∪∅∧a⁡x∈A∪∅∧b⁡x∈A∪∅→a⁡x=b⁡x↔¬a⁡xRb⁡x∨b⁡xRa⁡x
73 1 72 mpan ⊢a⁡x∈A∪∅∧b⁡x∈A∪∅→a⁡x=b⁡x↔¬a⁡xRb⁡x∨b⁡xRa⁡x
74 70 71 73 syl2an ⊢a∈F∧b∈F→a⁡x=b⁡x↔¬a⁡xRb⁡x∨b⁡xRa⁡x
75 74 imbi2d ⊢a∈F∧b∈F→∀y∈xa⁡y=b⁡y→a⁡x=b⁡x↔∀y∈xa⁡y=b⁡y→¬a⁡xRb⁡x∨b⁡xRa⁡x
76 75 ralbidv ⊢a∈F∧b∈F→∀x∈On∀y∈xa⁡y=b⁡y→a⁡x=b⁡x↔∀x∈On∀y∈xa⁡y=b⁡y→¬a⁡xRb⁡x∨b⁡xRa⁡x
77 vex ⊢y∈V
78 fveq2 ⊢x=y→a⁡x=a⁡y
79 fveq2 ⊢x=y→b⁡x=b⁡y
80 78 79 eqeq12d ⊢x=y→a⁡x=b⁡x↔a⁡y=b⁡y
81 77 80 sbcie ⊢[˙y/x]˙a⁡x=b⁡x↔a⁡y=b⁡y
82 81 ralbii ⊢∀y∈x[˙y/x]˙a⁡x=b⁡x↔∀y∈xa⁡y=b⁡y
83 82 imbi1i ⊢∀y∈x[˙y/x]˙a⁡x=b⁡x→a⁡x=b⁡x↔∀y∈xa⁡y=b⁡y→a⁡x=b⁡x
84 83 ralbii ⊢∀x∈On∀y∈x[˙y/x]˙a⁡x=b⁡x→a⁡x=b⁡x↔∀x∈On∀y∈xa⁡y=b⁡y→a⁡x=b⁡x
85 tfisg ⊢∀x∈On∀y∈x[˙y/x]˙a⁡x=b⁡x→a⁡x=b⁡x→∀x∈Ona⁡x=b⁡x
86 84 85 sylbir ⊢∀x∈On∀y∈xa⁡y=b⁡y→a⁡x=b⁡x→∀x∈Ona⁡x=b⁡x
87 vex ⊢a∈V
88 feq1 ⊢f=a→f:x⟶A↔a:x⟶A
89 88 rexbidv ⊢f=a→∃x∈Onf:x⟶A↔∃x∈Ona:x⟶A
90 87 89 2 elab2 ⊢a∈F↔∃x∈Ona:x⟶A
91 feq2 ⊢x=p→a:x⟶A↔a:p⟶A
92 91 cbvrexvw ⊢∃x∈Ona:x⟶A↔∃p∈Ona:p⟶A
93 90 92 bitri ⊢a∈F↔∃p∈Ona:p⟶A
94 vex ⊢b∈V
95 feq1 ⊢f=b→f:x⟶A↔b:x⟶A
96 95 rexbidv ⊢f=b→∃x∈Onf:x⟶A↔∃x∈Onb:x⟶A
97 94 96 2 elab2 ⊢b∈F↔∃x∈Onb:x⟶A
98 feq2 ⊢x=q→b:x⟶A↔b:q⟶A
99 98 cbvrexvw ⊢∃x∈Onb:x⟶A↔∃q∈Onb:q⟶A
100 97 99 bitri ⊢b∈F↔∃q∈Onb:q⟶A
101 93 100 anbi12i ⊢a∈F∧b∈F↔∃p∈Ona:p⟶A∧∃q∈Onb:q⟶A
102 reeanv ⊢∃p∈On∃q∈Ona:p⟶A∧b:q⟶A↔∃p∈Ona:p⟶A∧∃q∈Onb:q⟶A
103 101 102 bitr4i ⊢a∈F∧b∈F↔∃p∈On∃q∈Ona:p⟶A∧b:q⟶A
104 onss ⊢q∈On→q⊆On
105 ssralv ⊢q⊆On→∀x∈Ona⁡x=b⁡x→∀x∈qa⁡x=b⁡x
106 104 105 syl ⊢q∈On→∀x∈Ona⁡x=b⁡x→∀x∈qa⁡x=b⁡x
107 106 ad2antlr ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→∀x∈qa⁡x=b⁡x
108 fveq2 ⊢x=p→a⁡x=a⁡p
109 fveq2 ⊢x=p→b⁡x=b⁡p
110 108 109 eqeq12d ⊢x=p→a⁡x=b⁡x↔a⁡p=b⁡p
111 110 rspcv ⊢p∈q→∀x∈qa⁡x=b⁡x→a⁡p=b⁡p
112 111 a1i ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→p∈q→∀x∈qa⁡x=b⁡x→a⁡p=b⁡p
113 ffvelcdm ⊢b:q⟶A∧p∈q→b⁡p∈A
114 fdm ⊢a:p⟶A→dom⁡a=p
115 eloni ⊢p∈On→Ord⁡p
116 ordirr ⊢Ord⁡p→¬p∈p
117 115 116 syl ⊢p∈On→¬p∈p
118 eleq2 ⊢dom⁡a=p→p∈dom⁡a↔p∈p
119 118 notbid ⊢dom⁡a=p→¬p∈dom⁡a↔¬p∈p
120 119 biimparc ⊢¬p∈p∧dom⁡a=p→¬p∈dom⁡a
121 117 120 sylan ⊢p∈On∧dom⁡a=p→¬p∈dom⁡a
122 ndmfv ⊢¬p∈dom⁡a→a⁡p=∅
123 eqtr2 ⊢a⁡p=∅∧a⁡p=b⁡p→∅=b⁡p
124 eleq1 ⊢∅=b⁡p→∅∈A↔b⁡p∈A
125 124 biimprd ⊢∅=b⁡p→b⁡p∈A→∅∈A
126 123 125 syl ⊢a⁡p=∅∧a⁡p=b⁡p→b⁡p∈A→∅∈A
127 126 ex ⊢a⁡p=∅→a⁡p=b⁡p→b⁡p∈A→∅∈A
128 121 122 127 3syl ⊢p∈On∧dom⁡a=p→a⁡p=b⁡p→b⁡p∈A→∅∈A
129 128 com23 ⊢p∈On∧dom⁡a=p→b⁡p∈A→a⁡p=b⁡p→∅∈A
130 114 129 sylan2 ⊢p∈On∧a:p⟶A→b⁡p∈A→a⁡p=b⁡p→∅∈A
131 130 adantlr ⊢p∈On∧q∈On∧a:p⟶A→b⁡p∈A→a⁡p=b⁡p→∅∈A
132 113 131 syl5 ⊢p∈On∧q∈On∧a:p⟶A→b:q⟶A∧p∈q→a⁡p=b⁡p→∅∈A
133 132 exp4b ⊢p∈On∧q∈On→a:p⟶A→b:q⟶A→p∈q→a⁡p=b⁡p→∅∈A
134 133 imp32 ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→p∈q→a⁡p=b⁡p→∅∈A
135 112 134 syldd ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→p∈q→∀x∈qa⁡x=b⁡x→∅∈A
136 135 com23 ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈qa⁡x=b⁡x→p∈q→∅∈A
137 136 imp ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A∧∀x∈qa⁡x=b⁡x→p∈q→∅∈A
138 4 137 mtoi ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A∧∀x∈qa⁡x=b⁡x→¬p∈q
139 138 ex ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈qa⁡x=b⁡x→¬p∈q
140 107 139 syld ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→¬p∈q
141 onss ⊢p∈On→p⊆On
142 ssralv ⊢p⊆On→∀x∈Ona⁡x=b⁡x→∀x∈pa⁡x=b⁡x
143 141 142 syl ⊢p∈On→∀x∈Ona⁡x=b⁡x→∀x∈pa⁡x=b⁡x
144 143 ad2antrr ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→∀x∈pa⁡x=b⁡x
145 fveq2 ⊢x=q→a⁡x=a⁡q
146 fveq2 ⊢x=q→b⁡x=b⁡q
147 145 146 eqeq12d ⊢x=q→a⁡x=b⁡x↔a⁡q=b⁡q
148 147 rspcv ⊢q∈p→∀x∈pa⁡x=b⁡x→a⁡q=b⁡q
149 148 a1i ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→q∈p→∀x∈pa⁡x=b⁡x→a⁡q=b⁡q
150 ffvelcdm ⊢a:p⟶A∧q∈p→a⁡q∈A
151 fdm ⊢b:q⟶A→dom⁡b=q
152 eloni ⊢q∈On→Ord⁡q
153 ordirr ⊢Ord⁡q→¬q∈q
154 152 153 syl ⊢q∈On→¬q∈q
155 eleq2 ⊢dom⁡b=q→q∈dom⁡b↔q∈q
156 155 notbid ⊢dom⁡b=q→¬q∈dom⁡b↔¬q∈q
157 156 biimparc ⊢¬q∈q∧dom⁡b=q→¬q∈dom⁡b
158 ndmfv ⊢¬q∈dom⁡b→b⁡q=∅
159 157 158 syl ⊢¬q∈q∧dom⁡b=q→b⁡q=∅
160 154 159 sylan ⊢q∈On∧dom⁡b=q→b⁡q=∅
161 eqtr ⊢a⁡q=b⁡q∧b⁡q=∅→a⁡q=∅
162 eleq1 ⊢a⁡q=∅→a⁡q∈A↔∅∈A
163 162 biimpd ⊢a⁡q=∅→a⁡q∈A→∅∈A
164 161 163 syl ⊢a⁡q=b⁡q∧b⁡q=∅→a⁡q∈A→∅∈A
165 164 expcom ⊢b⁡q=∅→a⁡q=b⁡q→a⁡q∈A→∅∈A
166 165 com23 ⊢b⁡q=∅→a⁡q∈A→a⁡q=b⁡q→∅∈A
167 160 166 syl ⊢q∈On∧dom⁡b=q→a⁡q∈A→a⁡q=b⁡q→∅∈A
168 167 adantll ⊢p∈On∧q∈On∧dom⁡b=q→a⁡q∈A→a⁡q=b⁡q→∅∈A
169 151 168 sylan2 ⊢p∈On∧q∈On∧b:q⟶A→a⁡q∈A→a⁡q=b⁡q→∅∈A
170 150 169 syl5 ⊢p∈On∧q∈On∧b:q⟶A→a:p⟶A∧q∈p→a⁡q=b⁡q→∅∈A
171 170 exp4b ⊢p∈On∧q∈On→b:q⟶A→a:p⟶A→q∈p→a⁡q=b⁡q→∅∈A
172 171 com23 ⊢p∈On∧q∈On→a:p⟶A→b:q⟶A→q∈p→a⁡q=b⁡q→∅∈A
173 172 imp32 ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→q∈p→a⁡q=b⁡q→∅∈A
174 149 173 syldd ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→q∈p→∀x∈pa⁡x=b⁡x→∅∈A
175 174 com23 ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈pa⁡x=b⁡x→q∈p→∅∈A
176 175 imp ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A∧∀x∈pa⁡x=b⁡x→q∈p→∅∈A
177 4 176 mtoi ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A∧∀x∈pa⁡x=b⁡x→¬q∈p
178 177 ex ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈pa⁡x=b⁡x→¬q∈p
179 144 178 syld ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→¬q∈p
180 140 179 jcad ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→¬p∈q∧¬q∈p
181 ordtri3or ⊢Ord⁡p∧Ord⁡q→p∈q∨p=q∨q∈p
182 115 152 181 syl2an ⊢p∈On∧q∈On→p∈q∨p=q∨q∈p
183 182 adantr ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→p∈q∨p=q∨q∈p
184 3orel13 ⊢¬p∈q∧¬q∈p→p∈q∨p=q∨q∈p→p=q
185 180 183 184 syl6ci ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→p=q
186 185 144 jcad ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→p=q∧∀x∈pa⁡x=b⁡x
187 ffn ⊢a:p⟶A→aFnp
188 ffn ⊢b:q⟶A→bFnq
189 eqfnfv2 ⊢aFnp∧bFnq→a=b↔p=q∧∀x∈pa⁡x=b⁡x
190 187 188 189 syl2an ⊢a:p⟶A∧b:q⟶A→a=b↔p=q∧∀x∈pa⁡x=b⁡x
191 190 adantl ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→a=b↔p=q∧∀x∈pa⁡x=b⁡x
192 186 191 sylibrd ⊢p∈On∧q∈On∧a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→a=b
193 192 ex ⊢p∈On∧q∈On→a:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→a=b
194 193 rexlimivv ⊢∃p∈On∃q∈Ona:p⟶A∧b:q⟶A→∀x∈Ona⁡x=b⁡x→a=b
195 103 194 sylbi ⊢a∈F∧b∈F→∀x∈Ona⁡x=b⁡x→a=b
196 86 195 syl5 ⊢a∈F∧b∈F→∀x∈On∀y∈xa⁡y=b⁡y→a⁡x=b⁡x→a=b
197 76 196 sylbird ⊢a∈F∧b∈F→∀x∈On∀y∈xa⁡y=b⁡y→¬a⁡xRb⁡x∨b⁡xRa⁡x→a=b
198 65 197 biimtrrid ⊢a∈F∧b∈F→¬∃x∈On∀y∈xa⁡y=b⁡y∧a⁡xRb⁡x∨∃x∈On∀y∈xb⁡y=a⁡y∧b⁡xRa⁡x→a=b
199 54 198 sylbid ⊢a∈F∧b∈F→¬aSb∨bSa→a=b
200 199 orrd ⊢a∈F∧b∈F→aSb∨bSa∨a=b
201 3orcomb ⊢aSb∨a=b∨bSa↔aSb∨bSa∨a=b
202 df-3or ⊢aSb∨bSa∨a=b↔aSb∨bSa∨a=b
203 201 202 bitr2i ⊢aSb∨bSa∨a=b↔aSb∨a=b∨bSa
204 200 203 sylib ⊢a∈F∧b∈F→aSb∨a=b∨bSa
205 204 rgen2 ⊢∀a∈F∀b∈FaSb∨a=b∨bSa
206 df-so ⊢SOrF↔SPoF∧∀a∈F∀b∈FaSb∨a=b∨bSa
207 7 205 206 mpbir2an ⊢SOrF