Metamath Proof Explorer

Theorem poseq

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

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

Proof

Step Hyp Ref Expression
1 poseq.1 ⊢RPoA∪∅
2 poseq.2 ⊢F=f|∃x∈Onf:x⟶A
3 poseq.3 ⊢S=fg|f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x
4 feq2 ⊢x=b→f:x⟶A↔f:b⟶A
5 4 cbvrexvw ⊢∃x∈Onf:x⟶A↔∃b∈Onf:b⟶A
6 5 abbii ⊢f|∃x∈Onf:x⟶A=f|∃b∈Onf:b⟶A
7 2 6 eqtri ⊢F=f|∃b∈Onf:b⟶A
8 7 orderseqlem ⊢a∈F→a⁡x∈A∪∅
9 poirr ⊢RPoA∪∅∧a⁡x∈A∪∅→¬a⁡xRa⁡x
10 1 8 9 sylancr ⊢a∈F→¬a⁡xRa⁡x
11 10 intnand ⊢a∈F→¬∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
12 11 adantr ⊢a∈F∧x∈On→¬∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
13 12 nrexdv ⊢a∈F→¬∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
14 13 adantr ⊢a∈F∧a∈F→¬∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
15 imnan ⊢a∈F∧a∈F→¬∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x↔¬a∈F∧a∈F∧∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
16 14 15 mpbi ⊢¬a∈F∧a∈F∧∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
17 vex ⊢a∈V
18 eleq1w ⊢f=a→f∈F↔a∈F
19 18 anbi1d ⊢f=a→f∈F∧g∈F↔a∈F∧g∈F
20 fveq1 ⊢f=a→f⁡y=a⁡y
21 20 eqeq1d ⊢f=a→f⁡y=g⁡y↔a⁡y=g⁡y
22 21 ralbidv ⊢f=a→∀y∈xf⁡y=g⁡y↔∀y∈xa⁡y=g⁡y
23 fveq1 ⊢f=a→f⁡x=a⁡x
24 23 breq1d ⊢f=a→f⁡xRg⁡x↔a⁡xRg⁡x
25 22 24 anbi12d ⊢f=a→∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x
26 25 rexbidv ⊢f=a→∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃x∈On∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x
27 19 26 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
28 eleq1w ⊢g=a→g∈F↔a∈F
29 28 anbi2d ⊢g=a→a∈F∧g∈F↔a∈F∧a∈F
30 fveq1 ⊢g=a→g⁡y=a⁡y
31 30 eqeq2d ⊢g=a→a⁡y=g⁡y↔a⁡y=a⁡y
32 31 ralbidv ⊢g=a→∀y∈xa⁡y=g⁡y↔∀y∈xa⁡y=a⁡y
33 fveq1 ⊢g=a→g⁡x=a⁡x
34 33 breq2d ⊢g=a→a⁡xRg⁡x↔a⁡xRa⁡x
35 32 34 anbi12d ⊢g=a→∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x↔∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
36 35 rexbidv ⊢g=a→∃x∈On∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x↔∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
37 29 36 anbi12d ⊢g=a→a∈F∧g∈F∧∃x∈On∀y∈xa⁡y=g⁡y∧a⁡xRg⁡x↔a∈F∧a∈F∧∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
38 17 17 27 37 3 brab ⊢aSa↔a∈F∧a∈F∧∃x∈On∀y∈xa⁡y=a⁡y∧a⁡xRa⁡x
39 16 38 mtbir ⊢¬aSa
40 vex ⊢b∈V
41 raleq ⊢x=z→∀y∈xf⁡y=g⁡y↔∀y∈zf⁡y=g⁡y
42 fveq2 ⊢x=z→f⁡x=f⁡z
43 fveq2 ⊢x=z→g⁡x=g⁡z
44 42 43 breq12d ⊢x=z→f⁡xRg⁡x↔f⁡zRg⁡z
45 41 44 anbi12d ⊢x=z→∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∀y∈zf⁡y=g⁡y∧f⁡zRg⁡z
46 45 cbvrexvw ⊢∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃z∈On∀y∈zf⁡y=g⁡y∧f⁡zRg⁡z
47 21 ralbidv ⊢f=a→∀y∈zf⁡y=g⁡y↔∀y∈za⁡y=g⁡y
48 fveq1 ⊢f=a→f⁡z=a⁡z
49 48 breq1d ⊢f=a→f⁡zRg⁡z↔a⁡zRg⁡z
50 47 49 anbi12d ⊢f=a→∀y∈zf⁡y=g⁡y∧f⁡zRg⁡z↔∀y∈za⁡y=g⁡y∧a⁡zRg⁡z
51 50 rexbidv ⊢f=a→∃z∈On∀y∈zf⁡y=g⁡y∧f⁡zRg⁡z↔∃z∈On∀y∈za⁡y=g⁡y∧a⁡zRg⁡z
52 46 51 bitrid ⊢f=a→∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃z∈On∀y∈za⁡y=g⁡y∧a⁡zRg⁡z
53 19 52 anbi12d ⊢f=a→f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔a∈F∧g∈F∧∃z∈On∀y∈za⁡y=g⁡y∧a⁡zRg⁡z
54 eleq1w ⊢g=b→g∈F↔b∈F
55 54 anbi2d ⊢g=b→a∈F∧g∈F↔a∈F∧b∈F
56 fveq1 ⊢g=b→g⁡y=b⁡y
57 56 eqeq2d ⊢g=b→a⁡y=g⁡y↔a⁡y=b⁡y
58 57 ralbidv ⊢g=b→∀y∈za⁡y=g⁡y↔∀y∈za⁡y=b⁡y
59 fveq1 ⊢g=b→g⁡z=b⁡z
60 59 breq2d ⊢g=b→a⁡zRg⁡z↔a⁡zRb⁡z
61 58 60 anbi12d ⊢g=b→∀y∈za⁡y=g⁡y∧a⁡zRg⁡z↔∀y∈za⁡y=b⁡y∧a⁡zRb⁡z
62 61 rexbidv ⊢g=b→∃z∈On∀y∈za⁡y=g⁡y∧a⁡zRg⁡z↔∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z
63 55 62 anbi12d ⊢g=b→a∈F∧g∈F∧∃z∈On∀y∈za⁡y=g⁡y∧a⁡zRg⁡z↔a∈F∧b∈F∧∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z
64 17 40 53 63 3 brab ⊢aSb↔a∈F∧b∈F∧∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z
65 vex ⊢c∈V
66 eleq1w ⊢f=b→f∈F↔b∈F
67 66 anbi1d ⊢f=b→f∈F∧g∈F↔b∈F∧g∈F
68 raleq ⊢x=w→∀y∈xf⁡y=g⁡y↔∀y∈wf⁡y=g⁡y
69 fveq2 ⊢x=w→f⁡x=f⁡w
70 fveq2 ⊢x=w→g⁡x=g⁡w
71 69 70 breq12d ⊢x=w→f⁡xRg⁡x↔f⁡wRg⁡w
72 68 71 anbi12d ⊢x=w→∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∀y∈wf⁡y=g⁡y∧f⁡wRg⁡w
73 72 cbvrexvw ⊢∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃w∈On∀y∈wf⁡y=g⁡y∧f⁡wRg⁡w
74 fveq1 ⊢f=b→f⁡y=b⁡y
75 74 eqeq1d ⊢f=b→f⁡y=g⁡y↔b⁡y=g⁡y
76 75 ralbidv ⊢f=b→∀y∈wf⁡y=g⁡y↔∀y∈wb⁡y=g⁡y
77 fveq1 ⊢f=b→f⁡w=b⁡w
78 77 breq1d ⊢f=b→f⁡wRg⁡w↔b⁡wRg⁡w
79 76 78 anbi12d ⊢f=b→∀y∈wf⁡y=g⁡y∧f⁡wRg⁡w↔∀y∈wb⁡y=g⁡y∧b⁡wRg⁡w
80 79 rexbidv ⊢f=b→∃w∈On∀y∈wf⁡y=g⁡y∧f⁡wRg⁡w↔∃w∈On∀y∈wb⁡y=g⁡y∧b⁡wRg⁡w
81 73 80 bitrid ⊢f=b→∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃w∈On∀y∈wb⁡y=g⁡y∧b⁡wRg⁡w
82 67 81 anbi12d ⊢f=b→f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔b∈F∧g∈F∧∃w∈On∀y∈wb⁡y=g⁡y∧b⁡wRg⁡w
83 eleq1w ⊢g=c→g∈F↔c∈F
84 83 anbi2d ⊢g=c→b∈F∧g∈F↔b∈F∧c∈F
85 fveq1 ⊢g=c→g⁡y=c⁡y
86 85 eqeq2d ⊢g=c→b⁡y=g⁡y↔b⁡y=c⁡y
87 86 ralbidv ⊢g=c→∀y∈wb⁡y=g⁡y↔∀y∈wb⁡y=c⁡y
88 fveq1 ⊢g=c→g⁡w=c⁡w
89 88 breq2d ⊢g=c→b⁡wRg⁡w↔b⁡wRc⁡w
90 87 89 anbi12d ⊢g=c→∀y∈wb⁡y=g⁡y∧b⁡wRg⁡w↔∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
91 90 rexbidv ⊢g=c→∃w∈On∀y∈wb⁡y=g⁡y∧b⁡wRg⁡w↔∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
92 84 91 anbi12d ⊢g=c→b∈F∧g∈F∧∃w∈On∀y∈wb⁡y=g⁡y∧b⁡wRg⁡w↔b∈F∧c∈F∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
93 40 65 82 92 3 brab ⊢bSc↔b∈F∧c∈F∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
94 simplll ⊢a∈F∧b∈F∧b∈F∧c∈F∧∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w→a∈F
95 simplrr ⊢a∈F∧b∈F∧b∈F∧c∈F∧∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w→c∈F
96 an4 ⊢∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w↔∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
97 96 2rexbii ⊢∃z∈On∃w∈On∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w↔∃z∈On∃w∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
98 reeanv ⊢∃z∈On∃w∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w↔∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
99 97 98 bitri ⊢∃z∈On∃w∈On∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w↔∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w
100 eloni ⊢z∈On→Ord⁡z
101 eloni ⊢w∈On→Ord⁡w
102 ordtri3or ⊢Ord⁡z∧Ord⁡w→z∈w∨z=w∨w∈z
103 100 101 102 syl2an ⊢z∈On∧w∈On→z∈w∨z=w∨w∈z
104 simp1l ⊢z∈On∧w∈On∧z∈w∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→z∈On
105 onelss ⊢w∈On→z∈w→z⊆w
106 105 imp ⊢w∈On∧z∈w→z⊆w
107 106 adantll ⊢z∈On∧w∈On∧z∈w→z⊆w
108 ssralv ⊢z⊆w→∀y∈wb⁡y=c⁡y→∀y∈zb⁡y=c⁡y
109 108 anim2d ⊢z⊆w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y→∀y∈za⁡y=b⁡y∧∀y∈zb⁡y=c⁡y
110 r19.26 ⊢∀y∈za⁡y=b⁡y∧b⁡y=c⁡y↔∀y∈za⁡y=b⁡y∧∀y∈zb⁡y=c⁡y
111 109 110 syl6ibr ⊢z⊆w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y→∀y∈za⁡y=b⁡y∧b⁡y=c⁡y
112 eqtr ⊢a⁡y=b⁡y∧b⁡y=c⁡y→a⁡y=c⁡y
113 112 ralimi ⊢∀y∈za⁡y=b⁡y∧b⁡y=c⁡y→∀y∈za⁡y=c⁡y
114 111 113 syl6 ⊢z⊆w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y→∀y∈za⁡y=c⁡y
115 107 114 syl ⊢z∈On∧w∈On∧z∈w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y→∀y∈za⁡y=c⁡y
116 115 adantrd ⊢z∈On∧w∈On∧z∈w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→∀y∈za⁡y=c⁡y
117 116 3impia ⊢z∈On∧w∈On∧z∈w∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→∀y∈za⁡y=c⁡y
118 fveq2 ⊢y=z→b⁡y=b⁡z
119 fveq2 ⊢y=z→c⁡y=c⁡z
120 118 119 eqeq12d ⊢y=z→b⁡y=c⁡y↔b⁡z=c⁡z
121 120 rspcv ⊢z∈w→∀y∈wb⁡y=c⁡y→b⁡z=c⁡z
122 breq2 ⊢b⁡z=c⁡z→a⁡zRb⁡z↔a⁡zRc⁡z
123 122 biimpd ⊢b⁡z=c⁡z→a⁡zRb⁡z→a⁡zRc⁡z
124 121 123 syl6 ⊢z∈w→∀y∈wb⁡y=c⁡y→a⁡zRb⁡z→a⁡zRc⁡z
125 124 com3l ⊢∀y∈wb⁡y=c⁡y→a⁡zRb⁡z→z∈w→a⁡zRc⁡z
126 125 imp ⊢∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z→z∈w→a⁡zRc⁡z
127 126 ad2ant2lr ⊢∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→z∈w→a⁡zRc⁡z
128 127 impcom ⊢z∈w∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a⁡zRc⁡z
129 128 3adant1 ⊢z∈On∧w∈On∧z∈w∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a⁡zRc⁡z
130 raleq ⊢t=z→∀y∈ta⁡y=c⁡y↔∀y∈za⁡y=c⁡y
131 fveq2 ⊢t=z→a⁡t=a⁡z
132 fveq2 ⊢t=z→c⁡t=c⁡z
133 131 132 breq12d ⊢t=z→a⁡tRc⁡t↔a⁡zRc⁡z
134 130 133 anbi12d ⊢t=z→∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t↔∀y∈za⁡y=c⁡y∧a⁡zRc⁡z
135 134 rspcev ⊢z∈On∧∀y∈za⁡y=c⁡y∧a⁡zRc⁡z→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
136 104 117 129 135 syl12anc ⊢z∈On∧w∈On∧z∈w∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
137 136 a1d ⊢z∈On∧w∈On∧z∈w∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
138 137 3exp ⊢z∈On∧w∈On→z∈w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
139 2 orderseqlem ⊢a∈F→a⁡z∈A∪∅
140 139 ad2antrr ⊢a∈F∧b∈F∧b∈F∧c∈F→a⁡z∈A∪∅
141 2 orderseqlem ⊢b∈F→b⁡z∈A∪∅
142 141 ad2antlr ⊢a∈F∧b∈F∧b∈F∧c∈F→b⁡z∈A∪∅
143 2 orderseqlem ⊢c∈F→c⁡z∈A∪∅
144 143 ad2antll ⊢a∈F∧b∈F∧b∈F∧c∈F→c⁡z∈A∪∅
145 140 142 144 3jca ⊢a∈F∧b∈F∧b∈F∧c∈F→a⁡z∈A∪∅∧b⁡z∈A∪∅∧c⁡z∈A∪∅
146 potr ⊢RPoA∪∅∧a⁡z∈A∪∅∧b⁡z∈A∪∅∧c⁡z∈A∪∅→a⁡zRb⁡z∧b⁡zRc⁡z→a⁡zRc⁡z
147 1 145 146 sylancr ⊢a∈F∧b∈F∧b∈F∧c∈F→a⁡zRb⁡z∧b⁡zRc⁡z→a⁡zRc⁡z
148 147 impcom ⊢a⁡zRb⁡z∧b⁡zRc⁡z∧a∈F∧b∈F∧b∈F∧c∈F→a⁡zRc⁡z
149 113 148 anim12i ⊢∀y∈za⁡y=b⁡y∧b⁡y=c⁡y∧a⁡zRb⁡z∧b⁡zRc⁡z∧a∈F∧b∈F∧b∈F∧c∈F→∀y∈za⁡y=c⁡y∧a⁡zRc⁡z
150 149 anassrs ⊢∀y∈za⁡y=b⁡y∧b⁡y=c⁡y∧a⁡zRb⁡z∧b⁡zRc⁡z∧a∈F∧b∈F∧b∈F∧c∈F→∀y∈za⁡y=c⁡y∧a⁡zRc⁡z
151 150 135 sylan2 ⊢z∈On∧∀y∈za⁡y=b⁡y∧b⁡y=c⁡y∧a⁡zRb⁡z∧b⁡zRc⁡z∧a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
152 151 exp32 ⊢z∈On→∀y∈za⁡y=b⁡y∧b⁡y=c⁡y∧a⁡zRb⁡z∧b⁡zRc⁡z→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
153 raleq ⊢z=w→∀y∈zb⁡y=c⁡y↔∀y∈wb⁡y=c⁡y
154 153 anbi2d ⊢z=w→∀y∈za⁡y=b⁡y∧∀y∈zb⁡y=c⁡y↔∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y
155 110 154 bitrid ⊢z=w→∀y∈za⁡y=b⁡y∧b⁡y=c⁡y↔∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y
156 fveq2 ⊢z=w→b⁡z=b⁡w
157 fveq2 ⊢z=w→c⁡z=c⁡w
158 156 157 breq12d ⊢z=w→b⁡zRc⁡z↔b⁡wRc⁡w
159 158 anbi2d ⊢z=w→a⁡zRb⁡z∧b⁡zRc⁡z↔a⁡zRb⁡z∧b⁡wRc⁡w
160 155 159 anbi12d ⊢z=w→∀y∈za⁡y=b⁡y∧b⁡y=c⁡y∧a⁡zRb⁡z∧b⁡zRc⁡z↔∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w
161 160 imbi1d ⊢z=w→∀y∈za⁡y=b⁡y∧b⁡y=c⁡y∧a⁡zRb⁡z∧b⁡zRc⁡z→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t↔∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
162 152 161 syl5ibcom ⊢z∈On→z=w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
163 162 adantr ⊢z∈On∧w∈On→z=w→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
164 simp1r ⊢z∈On∧w∈On∧w∈z∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→w∈On
165 onelss ⊢z∈On→w∈z→w⊆z
166 165 imp ⊢z∈On∧w∈z→w⊆z
167 166 adantlr ⊢z∈On∧w∈On∧w∈z→w⊆z
168 ssralv ⊢w⊆z→∀y∈za⁡y=b⁡y→∀y∈wa⁡y=b⁡y
169 168 anim1d ⊢w⊆z→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y→∀y∈wa⁡y=b⁡y∧∀y∈wb⁡y=c⁡y
170 r19.26 ⊢∀y∈wa⁡y=b⁡y∧b⁡y=c⁡y↔∀y∈wa⁡y=b⁡y∧∀y∈wb⁡y=c⁡y
171 112 ralimi ⊢∀y∈wa⁡y=b⁡y∧b⁡y=c⁡y→∀y∈wa⁡y=c⁡y
172 170 171 sylbir ⊢∀y∈wa⁡y=b⁡y∧∀y∈wb⁡y=c⁡y→∀y∈wa⁡y=c⁡y
173 169 172 syl6 ⊢w⊆z→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y→∀y∈wa⁡y=c⁡y
174 173 adantrd ⊢w⊆z→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→∀y∈wa⁡y=c⁡y
175 167 174 syl ⊢z∈On∧w∈On∧w∈z→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→∀y∈wa⁡y=c⁡y
176 175 3impia ⊢z∈On∧w∈On∧w∈z∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→∀y∈wa⁡y=c⁡y
177 fveq2 ⊢y=w→a⁡y=a⁡w
178 fveq2 ⊢y=w→b⁡y=b⁡w
179 177 178 eqeq12d ⊢y=w→a⁡y=b⁡y↔a⁡w=b⁡w
180 179 rspcv ⊢w∈z→∀y∈za⁡y=b⁡y→a⁡w=b⁡w
181 breq1 ⊢a⁡w=b⁡w→a⁡wRc⁡w↔b⁡wRc⁡w
182 181 biimprd ⊢a⁡w=b⁡w→b⁡wRc⁡w→a⁡wRc⁡w
183 180 182 syl6 ⊢w∈z→∀y∈za⁡y=b⁡y→b⁡wRc⁡w→a⁡wRc⁡w
184 183 com3l ⊢∀y∈za⁡y=b⁡y→b⁡wRc⁡w→w∈z→a⁡wRc⁡w
185 184 imp ⊢∀y∈za⁡y=b⁡y∧b⁡wRc⁡w→w∈z→a⁡wRc⁡w
186 185 ad2ant2rl ⊢∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→w∈z→a⁡wRc⁡w
187 186 impcom ⊢w∈z∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a⁡wRc⁡w
188 187 3adant1 ⊢z∈On∧w∈On∧w∈z∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a⁡wRc⁡w
189 raleq ⊢t=w→∀y∈ta⁡y=c⁡y↔∀y∈wa⁡y=c⁡y
190 fveq2 ⊢t=w→a⁡t=a⁡w
191 fveq2 ⊢t=w→c⁡t=c⁡w
192 190 191 breq12d ⊢t=w→a⁡tRc⁡t↔a⁡wRc⁡w
193 189 192 anbi12d ⊢t=w→∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t↔∀y∈wa⁡y=c⁡y∧a⁡wRc⁡w
194 193 rspcev ⊢w∈On∧∀y∈wa⁡y=c⁡y∧a⁡wRc⁡w→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
195 164 176 188 194 syl12anc ⊢z∈On∧w∈On∧w∈z∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
196 195 a1d ⊢z∈On∧w∈On∧w∈z∧∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
197 196 3exp ⊢z∈On∧w∈On→w∈z→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
198 138 163 197 3jaod ⊢z∈On∧w∈On→z∈w∨z=w∨w∈z→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
199 103 198 mpd ⊢z∈On∧w∈On→∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
200 199 rexlimivv ⊢∃z∈On∃w∈On∀y∈za⁡y=b⁡y∧∀y∈wb⁡y=c⁡y∧a⁡zRb⁡z∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
201 99 200 sylbir ⊢∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w→a∈F∧b∈F∧b∈F∧c∈F→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
202 201 impcom ⊢a∈F∧b∈F∧b∈F∧c∈F∧∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w→∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
203 94 95 202 jca31 ⊢a∈F∧b∈F∧b∈F∧c∈F∧∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w→a∈F∧c∈F∧∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
204 203 an4s ⊢a∈F∧b∈F∧∃z∈On∀y∈za⁡y=b⁡y∧a⁡zRb⁡z∧b∈F∧c∈F∧∃w∈On∀y∈wb⁡y=c⁡y∧b⁡wRc⁡w→a∈F∧c∈F∧∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
205 64 93 204 syl2anb ⊢aSb∧bSc→a∈F∧c∈F∧∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
206 raleq ⊢x=t→∀y∈xf⁡y=g⁡y↔∀y∈tf⁡y=g⁡y
207 fveq2 ⊢x=t→f⁡x=f⁡t
208 fveq2 ⊢x=t→g⁡x=g⁡t
209 207 208 breq12d ⊢x=t→f⁡xRg⁡x↔f⁡tRg⁡t
210 206 209 anbi12d ⊢x=t→∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∀y∈tf⁡y=g⁡y∧f⁡tRg⁡t
211 210 cbvrexvw ⊢∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃t∈On∀y∈tf⁡y=g⁡y∧f⁡tRg⁡t
212 21 ralbidv ⊢f=a→∀y∈tf⁡y=g⁡y↔∀y∈ta⁡y=g⁡y
213 fveq1 ⊢f=a→f⁡t=a⁡t
214 213 breq1d ⊢f=a→f⁡tRg⁡t↔a⁡tRg⁡t
215 212 214 anbi12d ⊢f=a→∀y∈tf⁡y=g⁡y∧f⁡tRg⁡t↔∀y∈ta⁡y=g⁡y∧a⁡tRg⁡t
216 215 rexbidv ⊢f=a→∃t∈On∀y∈tf⁡y=g⁡y∧f⁡tRg⁡t↔∃t∈On∀y∈ta⁡y=g⁡y∧a⁡tRg⁡t
217 211 216 bitrid ⊢f=a→∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔∃t∈On∀y∈ta⁡y=g⁡y∧a⁡tRg⁡t
218 19 217 anbi12d ⊢f=a→f∈F∧g∈F∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡xRg⁡x↔a∈F∧g∈F∧∃t∈On∀y∈ta⁡y=g⁡y∧a⁡tRg⁡t
219 83 anbi2d ⊢g=c→a∈F∧g∈F↔a∈F∧c∈F
220 85 eqeq2d ⊢g=c→a⁡y=g⁡y↔a⁡y=c⁡y
221 220 ralbidv ⊢g=c→∀y∈ta⁡y=g⁡y↔∀y∈ta⁡y=c⁡y
222 fveq1 ⊢g=c→g⁡t=c⁡t
223 222 breq2d ⊢g=c→a⁡tRg⁡t↔a⁡tRc⁡t
224 221 223 anbi12d ⊢g=c→∀y∈ta⁡y=g⁡y∧a⁡tRg⁡t↔∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
225 224 rexbidv ⊢g=c→∃t∈On∀y∈ta⁡y=g⁡y∧a⁡tRg⁡t↔∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
226 219 225 anbi12d ⊢g=c→a∈F∧g∈F∧∃t∈On∀y∈ta⁡y=g⁡y∧a⁡tRg⁡t↔a∈F∧c∈F∧∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
227 17 65 218 226 3 brab ⊢aSc↔a∈F∧c∈F∧∃t∈On∀y∈ta⁡y=c⁡y∧a⁡tRc⁡t
228 205 227 sylibr ⊢aSb∧bSc→aSc
229 39 228 pm3.2i ⊢¬aSa∧aSb∧bSc→aSc
230 229 a1i ⊢a∈F∧b∈F∧c∈F→¬aSa∧aSb∧bSc→aSc
231 230 rgen3 ⊢∀a∈F∀b∈F∀c∈F¬aSa∧aSb∧bSc→aSc
232 df-po ⊢SPoF↔∀a∈F∀b∈F∀c∈F¬aSa∧aSb∧bSc→aSc
233 231 232 mpbir ⊢SPoF