Metamath Proof Explorer

Theorem soseq

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

Ref Expression
Hypotheses soseq.1 
|- R Or ( A u. { (/) } )
soseq.2 
|- F = { f | E. x e. On f : x --> A }
soseq.3 
|- S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) ) }
soseq.4 
|- -. (/) e. A
Assertion soseq 
|- S Or F

Proof

Step Hyp Ref Expression
1 soseq.1 
 |-  R Or ( A u. { (/) } )
2 soseq.2 
 |-  F = { f | E. x e. On f : x --> A }
3 soseq.3 
 |-  S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) ) }
4 soseq.4 
 |-  -. (/) e. A
5 sopo 
 |-  ( R Or ( A u. { (/) } ) -> R Po ( A u. { (/) } ) )
6 1 5 ax-mp 
 |-  R Po ( A u. { (/) } )
7 6 2 3 poseq 
 |-  S Po F
8 eleq1w 
 |-  ( f = a -> ( f e. F <-> a e. F ) )
9 8 anbi1d 
 |-  ( f = a -> ( ( f e. F /\ g e. F ) <-> ( a e. F /\ g e. 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 -> ( A. y e. x ( f ` y ) = ( g ` y ) <-> A. y e. x ( a ` y ) = ( g ` y ) ) )
13 fveq1 
 |-  ( f = a -> ( f ` x ) = ( a ` x ) )
14 13 breq1d 
 |-  ( f = a -> ( ( f ` x ) R ( g ` x ) <-> ( a ` x ) R ( g ` x ) ) )
15 12 14 anbi12d 
 |-  ( f = a -> ( ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) <-> ( A. y e. x ( a ` y ) = ( g ` y ) /\ ( a ` x ) R ( g ` x ) ) ) )
16 15 rexbidv 
 |-  ( f = a -> ( E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) <-> E. x e. On ( A. y e. x ( a ` y ) = ( g ` y ) /\ ( a ` x ) R ( g ` x ) ) ) )
17 9 16 anbi12d 
 |-  ( f = a -> ( ( ( f e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) ) <-> ( ( a e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( a ` y ) = ( g ` y ) /\ ( a ` x ) R ( g ` x ) ) ) ) )
18 eleq1w 
 |-  ( g = b -> ( g e. F <-> b e. F ) )
19 18 anbi2d 
 |-  ( g = b -> ( ( a e. F /\ g e. F ) <-> ( a e. F /\ b e. 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 -> ( A. y e. x ( a ` y ) = ( g ` y ) <-> A. y e. x ( a ` y ) = ( b ` y ) ) )
23 fveq1 
 |-  ( g = b -> ( g ` x ) = ( b ` x ) )
24 23 breq2d 
 |-  ( g = b -> ( ( a ` x ) R ( g ` x ) <-> ( a ` x ) R ( b ` x ) ) )
25 22 24 anbi12d 
 |-  ( g = b -> ( ( A. y e. x ( a ` y ) = ( g ` y ) /\ ( a ` x ) R ( g ` x ) ) <-> ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) ) )
26 25 rexbidv 
 |-  ( g = b -> ( E. x e. On ( A. y e. x ( a ` y ) = ( g ` y ) /\ ( a ` x ) R ( g ` x ) ) <-> E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) ) )
27 19 26 anbi12d 
 |-  ( g = b -> ( ( ( a e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( a ` y ) = ( g ` y ) /\ ( a ` x ) R ( g ` x ) ) ) <-> ( ( a e. F /\ b e. F ) /\ E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) ) ) )
28 17 27 3 brabg 
 |-  ( ( a e. F /\ b e. F ) -> ( a S b <-> ( ( a e. F /\ b e. F ) /\ E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) ) ) )
29 28 bianabs 
 |-  ( ( a e. F /\ b e. F ) -> ( a S b <-> E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) ) )
30 eleq1w 
 |-  ( f = b -> ( f e. F <-> b e. F ) )
31 30 anbi1d 
 |-  ( f = b -> ( ( f e. F /\ g e. F ) <-> ( b e. F /\ g e. 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 -> ( A. y e. x ( f ` y ) = ( g ` y ) <-> A. y e. x ( b ` y ) = ( g ` y ) ) )
35 fveq1 
 |-  ( f = b -> ( f ` x ) = ( b ` x ) )
36 35 breq1d 
 |-  ( f = b -> ( ( f ` x ) R ( g ` x ) <-> ( b ` x ) R ( g ` x ) ) )
37 34 36 anbi12d 
 |-  ( f = b -> ( ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) <-> ( A. y e. x ( b ` y ) = ( g ` y ) /\ ( b ` x ) R ( g ` x ) ) ) )
38 37 rexbidv 
 |-  ( f = b -> ( E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) <-> E. x e. On ( A. y e. x ( b ` y ) = ( g ` y ) /\ ( b ` x ) R ( g ` x ) ) ) )
39 31 38 anbi12d 
 |-  ( f = b -> ( ( ( f e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) ) <-> ( ( b e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( b ` y ) = ( g ` y ) /\ ( b ` x ) R ( g ` x ) ) ) ) )
40 eleq1w 
 |-  ( g = a -> ( g e. F <-> a e. F ) )
41 40 anbi2d 
 |-  ( g = a -> ( ( b e. F /\ g e. F ) <-> ( b e. F /\ a e. 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 -> ( A. y e. x ( b ` y ) = ( g ` y ) <-> A. y e. x ( b ` y ) = ( a ` y ) ) )
45 fveq1 
 |-  ( g = a -> ( g ` x ) = ( a ` x ) )
46 45 breq2d 
 |-  ( g = a -> ( ( b ` x ) R ( g ` x ) <-> ( b ` x ) R ( a ` x ) ) )
47 44 46 anbi12d 
 |-  ( g = a -> ( ( A. y e. x ( b ` y ) = ( g ` y ) /\ ( b ` x ) R ( g ` x ) ) <-> ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
48 47 rexbidv 
 |-  ( g = a -> ( E. x e. On ( A. y e. x ( b ` y ) = ( g ` y ) /\ ( b ` x ) R ( g ` x ) ) <-> E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
49 41 48 anbi12d 
 |-  ( g = a -> ( ( ( b e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( b ` y ) = ( g ` y ) /\ ( b ` x ) R ( g ` x ) ) ) <-> ( ( b e. F /\ a e. F ) /\ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) ) )
50 39 49 3 brabg 
 |-  ( ( b e. F /\ a e. F ) -> ( b S a <-> ( ( b e. F /\ a e. F ) /\ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) ) )
51 50 bianabs 
 |-  ( ( b e. F /\ a e. F ) -> ( b S a <-> E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
52 51 ancoms 
 |-  ( ( a e. F /\ b e. F ) -> ( b S a <-> E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
53 29 52 orbi12d 
 |-  ( ( a e. F /\ b e. F ) -> ( ( a S b \/ b S a ) <-> ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) ) )
54 53 notbid 
 |-  ( ( a e. F /\ b e. F ) -> ( -. ( a S b \/ b S a ) <-> -. ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) ) )
55 ralinexa 
 |-  ( A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) <-> -. E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) )
56 andi 
 |-  ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) <-> ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
57 eqcom 
 |-  ( ( a ` y ) = ( b ` y ) <-> ( b ` y ) = ( a ` y ) )
58 57 ralbii 
 |-  ( A. y e. x ( a ` y ) = ( b ` y ) <-> A. y e. x ( b ` y ) = ( a ` y ) )
59 58 anbi1i 
 |-  ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( b ` x ) R ( a ` x ) ) <-> ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) )
60 59 orbi2i 
 |-  ( ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( b ` x ) R ( a ` x ) ) ) <-> ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
61 56 60 bitri 
 |-  ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) <-> ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
62 61 rexbii 
 |-  ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) <-> E. x e. On ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
63 r19.43 
 |-  ( E. x e. On ( ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) <-> ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
64 62 63 bitri 
 |-  ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) <-> ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
65 55 64 xchbinx 
 |-  ( A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) <-> -. ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) )
66 feq2 
 |-  ( x = y -> ( f : x --> A <-> f : y --> A ) )
67 66 cbvrexvw 
 |-  ( E. x e. On f : x --> A <-> E. y e. On f : y --> A )
68 67 abbii 
 |-  { f | E. x e. On f : x --> A } = { f | E. y e. On f : y --> A }
69 2 68 eqtri 
 |-  F = { f | E. y e. On f : y --> A }
70 69 orderseqlem 
 |-  ( a e. F -> ( a ` x ) e. ( A u. { (/) } ) )
71 69 orderseqlem 
 |-  ( b e. F -> ( b ` x ) e. ( A u. { (/) } ) )
72 sotrieq 
 |-  ( ( R Or ( A u. { (/) } ) /\ ( ( a ` x ) e. ( A u. { (/) } ) /\ ( b ` x ) e. ( A u. { (/) } ) ) ) -> ( ( a ` x ) = ( b ` x ) <-> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) )
73 1 72 mpan 
 |-  ( ( ( a ` x ) e. ( A u. { (/) } ) /\ ( b ` x ) e. ( A u. { (/) } ) ) -> ( ( a ` x ) = ( b ` x ) <-> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) )
74 70 71 73 syl2an 
 |-  ( ( a e. F /\ b e. F ) -> ( ( a ` x ) = ( b ` x ) <-> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) )
75 74 imbi2d 
 |-  ( ( a e. F /\ b e. F ) -> ( ( A. y e. x ( a ` y ) = ( b ` y ) -> ( a ` x ) = ( b ` x ) ) <-> ( A. y e. x ( a ` y ) = ( b ` y ) -> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) ) )
76 75 ralbidv 
 |-  ( ( a e. F /\ b e. F ) -> ( A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> ( a ` x ) = ( b ` x ) ) <-> A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) ) )
77 vex 
 |-  y e. _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 
 |-  ( A. y e. x [. y / x ]. ( a ` x ) = ( b ` x ) <-> A. y e. x ( a ` y ) = ( b ` y ) )
83 82 imbi1i 
 |-  ( ( A. y e. x [. y / x ]. ( a ` x ) = ( b ` x ) -> ( a ` x ) = ( b ` x ) ) <-> ( A. y e. x ( a ` y ) = ( b ` y ) -> ( a ` x ) = ( b ` x ) ) )
84 83 ralbii 
 |-  ( A. x e. On ( A. y e. x [. y / x ]. ( a ` x ) = ( b ` x ) -> ( a ` x ) = ( b ` x ) ) <-> A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> ( a ` x ) = ( b ` x ) ) )
85 tfisg 
 |-  ( A. x e. On ( A. y e. x [. y / x ]. ( a ` x ) = ( b ` x ) -> ( a ` x ) = ( b ` x ) ) -> A. x e. On ( a ` x ) = ( b ` x ) )
86 84 85 sylbir 
 |-  ( A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> ( a ` x ) = ( b ` x ) ) -> A. x e. On ( a ` x ) = ( b ` x ) )
87 vex 
 |-  a e. _V
88 feq1 
 |-  ( f = a -> ( f : x --> A <-> a : x --> A ) )
89 88 rexbidv 
 |-  ( f = a -> ( E. x e. On f : x --> A <-> E. x e. On a : x --> A ) )
90 87 89 2 elab2 
 |-  ( a e. F <-> E. x e. On a : x --> A )
91 feq2 
 |-  ( x = p -> ( a : x --> A <-> a : p --> A ) )
92 91 cbvrexvw 
 |-  ( E. x e. On a : x --> A <-> E. p e. On a : p --> A )
93 90 92 bitri 
 |-  ( a e. F <-> E. p e. On a : p --> A )
94 vex 
 |-  b e. _V
95 feq1 
 |-  ( f = b -> ( f : x --> A <-> b : x --> A ) )
96 95 rexbidv 
 |-  ( f = b -> ( E. x e. On f : x --> A <-> E. x e. On b : x --> A ) )
97 94 96 2 elab2 
 |-  ( b e. F <-> E. x e. On b : x --> A )
98 feq2 
 |-  ( x = q -> ( b : x --> A <-> b : q --> A ) )
99 98 cbvrexvw 
 |-  ( E. x e. On b : x --> A <-> E. q e. On b : q --> A )
100 97 99 bitri 
 |-  ( b e. F <-> E. q e. On b : q --> A )
101 93 100 anbi12i 
 |-  ( ( a e. F /\ b e. F ) <-> ( E. p e. On a : p --> A /\ E. q e. On b : q --> A ) )
102 reeanv 
 |-  ( E. p e. On E. q e. On ( a : p --> A /\ b : q --> A ) <-> ( E. p e. On a : p --> A /\ E. q e. On b : q --> A ) )
103 101 102 bitr4i 
 |-  ( ( a e. F /\ b e. F ) <-> E. p e. On E. q e. On ( a : p --> A /\ b : q --> A ) )
104 onss 
 |-  ( q e. On -> q C_ On )
105 ssralv 
 |-  ( q C_ On -> ( A. x e. On ( a ` x ) = ( b ` x ) -> A. x e. q ( a ` x ) = ( b ` x ) ) )
106 104 105 syl 
 |-  ( q e. On -> ( A. x e. On ( a ` x ) = ( b ` x ) -> A. x e. q ( a ` x ) = ( b ` x ) ) )
107 106 ad2antlr 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> A. x e. q ( a ` 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 e. q -> ( A. x e. q ( a ` x ) = ( b ` x ) -> ( a ` p ) = ( b ` p ) ) )
112 111 a1i 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( p e. q -> ( A. x e. q ( a ` x ) = ( b ` x ) -> ( a ` p ) = ( b ` p ) ) ) )
113 ffvelcdm 
 |-  ( ( b : q --> A /\ p e. q ) -> ( b ` p ) e. A )
114 fdm 
 |-  ( a : p --> A -> dom a = p )
115 eloni 
 |-  ( p e. On -> Ord p )
116 ordirr 
 |-  ( Ord p -> -. p e. p )
117 115 116 syl 
 |-  ( p e. On -> -. p e. p )
118 eleq2 
 |-  ( dom a = p -> ( p e. dom a <-> p e. p ) )
119 118 notbid 
 |-  ( dom a = p -> ( -. p e. dom a <-> -. p e. p ) )
120 119 biimparc 
 |-  ( ( -. p e. p /\ dom a = p ) -> -. p e. dom a )
121 117 120 sylan 
 |-  ( ( p e. On /\ dom a = p ) -> -. p e. dom a )
122 ndmfv 
 |-  ( -. p e. dom a -> ( a ` p ) = (/) )
123 eqtr2 
 |-  ( ( ( a ` p ) = (/) /\ ( a ` p ) = ( b ` p ) ) -> (/) = ( b ` p ) )
124 eleq1 
 |-  ( (/) = ( b ` p ) -> ( (/) e. A <-> ( b ` p ) e. A ) )
125 124 biimprd 
 |-  ( (/) = ( b ` p ) -> ( ( b ` p ) e. A -> (/) e. A ) )
126 123 125 syl 
 |-  ( ( ( a ` p ) = (/) /\ ( a ` p ) = ( b ` p ) ) -> ( ( b ` p ) e. A -> (/) e. A ) )
127 126 ex 
 |-  ( ( a ` p ) = (/) -> ( ( a ` p ) = ( b ` p ) -> ( ( b ` p ) e. A -> (/) e. A ) ) )
128 121 122 127 3syl 
 |-  ( ( p e. On /\ dom a = p ) -> ( ( a ` p ) = ( b ` p ) -> ( ( b ` p ) e. A -> (/) e. A ) ) )
129 128 com23 
 |-  ( ( p e. On /\ dom a = p ) -> ( ( b ` p ) e. A -> ( ( a ` p ) = ( b ` p ) -> (/) e. A ) ) )
130 114 129 sylan2 
 |-  ( ( p e. On /\ a : p --> A ) -> ( ( b ` p ) e. A -> ( ( a ` p ) = ( b ` p ) -> (/) e. A ) ) )
131 130 adantlr 
 |-  ( ( ( p e. On /\ q e. On ) /\ a : p --> A ) -> ( ( b ` p ) e. A -> ( ( a ` p ) = ( b ` p ) -> (/) e. A ) ) )
132 113 131 syl5 
 |-  ( ( ( p e. On /\ q e. On ) /\ a : p --> A ) -> ( ( b : q --> A /\ p e. q ) -> ( ( a ` p ) = ( b ` p ) -> (/) e. A ) ) )
133 132 exp4b 
 |-  ( ( p e. On /\ q e. On ) -> ( a : p --> A -> ( b : q --> A -> ( p e. q -> ( ( a ` p ) = ( b ` p ) -> (/) e. A ) ) ) ) )
134 133 imp32 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( p e. q -> ( ( a ` p ) = ( b ` p ) -> (/) e. A ) ) )
135 112 134 syldd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( p e. q -> ( A. x e. q ( a ` x ) = ( b ` x ) -> (/) e. A ) ) )
136 135 com23 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. q ( a ` x ) = ( b ` x ) -> ( p e. q -> (/) e. A ) ) )
137 136 imp 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) /\ A. x e. q ( a ` x ) = ( b ` x ) ) -> ( p e. q -> (/) e. A ) )
138 4 137 mtoi 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) /\ A. x e. q ( a ` x ) = ( b ` x ) ) -> -. p e. q )
139 138 ex 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. q ( a ` x ) = ( b ` x ) -> -. p e. q ) )
140 107 139 syld 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> -. p e. q ) )
141 onss 
 |-  ( p e. On -> p C_ On )
142 ssralv 
 |-  ( p C_ On -> ( A. x e. On ( a ` x ) = ( b ` x ) -> A. x e. p ( a ` x ) = ( b ` x ) ) )
143 141 142 syl 
 |-  ( p e. On -> ( A. x e. On ( a ` x ) = ( b ` x ) -> A. x e. p ( a ` x ) = ( b ` x ) ) )
144 143 ad2antrr 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> A. x e. p ( a ` 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 e. p -> ( A. x e. p ( a ` x ) = ( b ` x ) -> ( a ` q ) = ( b ` q ) ) )
149 148 a1i 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( q e. p -> ( A. x e. p ( a ` x ) = ( b ` x ) -> ( a ` q ) = ( b ` q ) ) ) )
150 ffvelcdm 
 |-  ( ( a : p --> A /\ q e. p ) -> ( a ` q ) e. A )
151 fdm 
 |-  ( b : q --> A -> dom b = q )
152 eloni 
 |-  ( q e. On -> Ord q )
153 ordirr 
 |-  ( Ord q -> -. q e. q )
154 152 153 syl 
 |-  ( q e. On -> -. q e. q )
155 eleq2 
 |-  ( dom b = q -> ( q e. dom b <-> q e. q ) )
156 155 notbid 
 |-  ( dom b = q -> ( -. q e. dom b <-> -. q e. q ) )
157 156 biimparc 
 |-  ( ( -. q e. q /\ dom b = q ) -> -. q e. dom b )
158 ndmfv 
 |-  ( -. q e. dom b -> ( b ` q ) = (/) )
159 157 158 syl 
 |-  ( ( -. q e. q /\ dom b = q ) -> ( b ` q ) = (/) )
160 154 159 sylan 
 |-  ( ( q e. On /\ dom b = q ) -> ( b ` q ) = (/) )
161 eqtr 
 |-  ( ( ( a ` q ) = ( b ` q ) /\ ( b ` q ) = (/) ) -> ( a ` q ) = (/) )
162 eleq1 
 |-  ( ( a ` q ) = (/) -> ( ( a ` q ) e. A <-> (/) e. A ) )
163 162 biimpd 
 |-  ( ( a ` q ) = (/) -> ( ( a ` q ) e. A -> (/) e. A ) )
164 161 163 syl 
 |-  ( ( ( a ` q ) = ( b ` q ) /\ ( b ` q ) = (/) ) -> ( ( a ` q ) e. A -> (/) e. A ) )
165 164 expcom 
 |-  ( ( b ` q ) = (/) -> ( ( a ` q ) = ( b ` q ) -> ( ( a ` q ) e. A -> (/) e. A ) ) )
166 165 com23 
 |-  ( ( b ` q ) = (/) -> ( ( a ` q ) e. A -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) )
167 160 166 syl 
 |-  ( ( q e. On /\ dom b = q ) -> ( ( a ` q ) e. A -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) )
168 167 adantll 
 |-  ( ( ( p e. On /\ q e. On ) /\ dom b = q ) -> ( ( a ` q ) e. A -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) )
169 151 168 sylan2 
 |-  ( ( ( p e. On /\ q e. On ) /\ b : q --> A ) -> ( ( a ` q ) e. A -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) )
170 150 169 syl5 
 |-  ( ( ( p e. On /\ q e. On ) /\ b : q --> A ) -> ( ( a : p --> A /\ q e. p ) -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) )
171 170 exp4b 
 |-  ( ( p e. On /\ q e. On ) -> ( b : q --> A -> ( a : p --> A -> ( q e. p -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) ) ) )
172 171 com23 
 |-  ( ( p e. On /\ q e. On ) -> ( a : p --> A -> ( b : q --> A -> ( q e. p -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) ) ) )
173 172 imp32 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( q e. p -> ( ( a ` q ) = ( b ` q ) -> (/) e. A ) ) )
174 149 173 syldd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( q e. p -> ( A. x e. p ( a ` x ) = ( b ` x ) -> (/) e. A ) ) )
175 174 com23 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. p ( a ` x ) = ( b ` x ) -> ( q e. p -> (/) e. A ) ) )
176 175 imp 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) /\ A. x e. p ( a ` x ) = ( b ` x ) ) -> ( q e. p -> (/) e. A ) )
177 4 176 mtoi 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) /\ A. x e. p ( a ` x ) = ( b ` x ) ) -> -. q e. p )
178 177 ex 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. p ( a ` x ) = ( b ` x ) -> -. q e. p ) )
179 144 178 syld 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> -. q e. p ) )
180 140 179 jcad 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> ( -. p e. q /\ -. q e. p ) ) )
181 ordtri3or 
 |-  ( ( Ord p /\ Ord q ) -> ( p e. q \/ p = q \/ q e. p ) )
182 115 152 181 syl2an 
 |-  ( ( p e. On /\ q e. On ) -> ( p e. q \/ p = q \/ q e. p ) )
183 182 adantr 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( p e. q \/ p = q \/ q e. p ) )
184 3orel13 
 |-  ( ( -. p e. q /\ -. q e. p ) -> ( ( p e. q \/ p = q \/ q e. p ) -> p = q ) )
185 180 183 184 syl6ci 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> p = q ) )
186 185 144 jcad 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> ( p = q /\ A. x e. p ( a ` x ) = ( b ` x ) ) ) )
187 ffn 
 |-  ( a : p --> A -> a Fn p )
188 ffn 
 |-  ( b : q --> A -> b Fn q )
189 eqfnfv2 
 |-  ( ( a Fn p /\ b Fn q ) -> ( a = b <-> ( p = q /\ A. x e. p ( a ` x ) = ( b ` x ) ) ) )
190 187 188 189 syl2an 
 |-  ( ( a : p --> A /\ b : q --> A ) -> ( a = b <-> ( p = q /\ A. x e. p ( a ` x ) = ( b ` x ) ) ) )
191 190 adantl 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( a = b <-> ( p = q /\ A. x e. p ( a ` x ) = ( b ` x ) ) ) )
192 186 191 sylibrd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a : p --> A /\ b : q --> A ) ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> a = b ) )
193 192 ex 
 |-  ( ( p e. On /\ q e. On ) -> ( ( a : p --> A /\ b : q --> A ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> a = b ) ) )
194 193 rexlimivv 
 |-  ( E. p e. On E. q e. On ( a : p --> A /\ b : q --> A ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> a = b ) )
195 103 194 sylbi 
 |-  ( ( a e. F /\ b e. F ) -> ( A. x e. On ( a ` x ) = ( b ` x ) -> a = b ) )
196 86 195 syl5 
 |-  ( ( a e. F /\ b e. F ) -> ( A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> ( a ` x ) = ( b ` x ) ) -> a = b ) )
197 76 196 sylbird 
 |-  ( ( a e. F /\ b e. F ) -> ( A. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) -> -. ( ( a ` x ) R ( b ` x ) \/ ( b ` x ) R ( a ` x ) ) ) -> a = b ) )
198 65 197 biimtrrid 
 |-  ( ( a e. F /\ b e. F ) -> ( -. ( E. x e. On ( A. y e. x ( a ` y ) = ( b ` y ) /\ ( a ` x ) R ( b ` x ) ) \/ E. x e. On ( A. y e. x ( b ` y ) = ( a ` y ) /\ ( b ` x ) R ( a ` x ) ) ) -> a = b ) )
199 54 198 sylbid 
 |-  ( ( a e. F /\ b e. F ) -> ( -. ( a S b \/ b S a ) -> a = b ) )
200 199 orrd 
 |-  ( ( a e. F /\ b e. F ) -> ( ( a S b \/ b S a ) \/ a = b ) )
201 3orcomb 
 |-  ( ( a S b \/ a = b \/ b S a ) <-> ( a S b \/ b S a \/ a = b ) )
202 df-3or 
 |-  ( ( a S b \/ b S a \/ a = b ) <-> ( ( a S b \/ b S a ) \/ a = b ) )
203 201 202 bitr2i 
 |-  ( ( ( a S b \/ b S a ) \/ a = b ) <-> ( a S b \/ a = b \/ b S a ) )
204 200 203 sylib 
 |-  ( ( a e. F /\ b e. F ) -> ( a S b \/ a = b \/ b S a ) )
205 204 rgen2 
 |-  A. a e. F A. b e. F ( a S b \/ a = b \/ b S a )
206 df-so 
 |-  ( S Or F <-> ( S Po F /\ A. a e. F A. b e. F ( a S b \/ a = b \/ b S a ) ) )
207 7 205 206 mpbir2an 
 |-  S Or F