Metamath Proof Explorer

Theorem noetalem1

Description: Lemma for noeta . Either S or T satisfies the final condition. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetalem1.1 
|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
noetalem1.2 
|- T = if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
noetalem1.3 
|- Z = ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
noetalem1.4 
|- W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
Assertion noetalem1 
|- ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( S e. No /\ ( A. a e. A a

Proof

Step Hyp Ref Expression
1 noetalem1.1 
 |-  S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2 noetalem1.2 
 |-  T = if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
3 noetalem1.3 
 |-  Z = ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
4 noetalem1.4 
 |-  W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
5 2 noinfno 
 |-  ( ( B C_ No /\ B e. _V ) -> T e. No )
6 5 adantl 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> T e. No )
7 nodmord 
 |-  ( T e. No -> Ord dom T )
8 6 7 syl 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> Ord dom T )
9 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
10 9 adantr 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> S e. No )
11 nodmord 
 |-  ( S e. No -> Ord dom S )
12 10 11 syl 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> Ord dom S )
13 ordtri2or2 
 |-  ( ( Ord dom T /\ Ord dom S ) -> ( dom T C_ dom S \/ dom S C_ dom T ) )
14 8 12 13 syl2anc 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> ( dom T C_ dom S \/ dom S C_ dom T ) )
15 ssequn2 
 |-  ( dom T C_ dom S <-> ( dom S u. dom T ) = dom S )
16 ssequn1 
 |-  ( dom S C_ dom T <-> ( dom S u. dom T ) = dom T )
17 15 16 orbi12i 
 |-  ( ( dom T C_ dom S \/ dom S C_ dom T ) <-> ( ( dom S u. dom T ) = dom S \/ ( dom S u. dom T ) = dom T ) )
18 14 17 sylib 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> ( ( dom S u. dom T ) = dom S \/ ( dom S u. dom T ) = dom T ) )
19 18 3adant3 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( dom S u. dom T ) = dom S \/ ( dom S u. dom T ) = dom T ) )
20 simplll 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> A C_ No )
21 simpllr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> A e. _V )
22 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> B e. _V )
23 simpr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> a e. A )
24 1 3 noetasuplem3 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ a e. A ) -> a
25 20 21 22 23 24 syl31anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ a e. A ) -> a
26 25 ralrimiva 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> A. a e. A a
27 26 3adant3 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A. a e. A a
28 1 3 noetasuplem4 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A. b e. B Z
29 27 28 jca 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( A. a e. A a
30 29 adantr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( A. a e. A a
31 simp1l 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A C_ No )
32 simp1r 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A e. _V )
33 simp2r 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  B e. _V )
34 1 3 noetasuplem1 
 |-  ( ( A C_ No /\ A e. _V /\ B e. _V ) -> Z e. No )
35 31 32 33 34 syl3anc 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  Z e. No )
36 1 2 nosupinfsep 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ Z e. No ) -> ( ( A. a e. A a  ( A. a e. A a
37 35 36 syld3an3 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a  ( A. a e. A a
38 37 adantr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a  ( A. a e. A a
39 simpr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( dom S u. dom T ) = dom S )
40 39 reseq2d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( Z |` ( dom S u. dom T ) ) = ( Z |` dom S ) )
41 simplll 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> A C_ No )
42 simpllr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> A e. _V )
43 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> B e. _V )
44 1 3 noetasuplem2 
 |-  ( ( A C_ No /\ A e. _V /\ B e. _V ) -> ( Z |` dom S ) = S )
45 41 42 43 44 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( Z |` dom S ) = S )
46 40 45 eqtrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( Z |` ( dom S u. dom T ) ) = S )
47 46 breq2d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( a  a
48 47 ralbidv 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( A. a e. A a  A. a e. A a
49 46 breq1d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( ( Z |` ( dom S u. dom T ) )  S
50 49 ralbidv 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( A. b e. B ( Z |` ( dom S u. dom T ) )  A. b e. B S
51 48 50 anbi12d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom S ) -> ( ( A. a e. A a  ( A. a e. A a
52 51 3adantl3 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a  ( A. a e. A a
53 38 52 bitrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a  ( A. a e. A a
54 30 53 mpbid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( A. a e. A a
55 54 ex 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( dom S u. dom T ) = dom S -> ( A. a e. A a
56 2 4 noetainflem4 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A. a e. A a
57 simpllr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> A e. _V )
58 simplrl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> B C_ No )
59 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> B e. _V )
60 simpr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> b e. B )
61 2 4 noetainflem3 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ b e. B ) -> W
62 57 58 59 60 61 syl31anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ b e. B ) -> W
63 62 ralrimiva 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) -> A. b e. B W
64 63 3adant3 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A. b e. B W
65 56 64 jca 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( A. a e. A a
66 65 adantr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( A. a e. A a
67 simpl1 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( A C_ No /\ A e. _V ) )
68 simpl2l 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  B C_ No )
69 simpl2r 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  B e. _V )
70 simpl1r 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  A e. _V )
71 2 4 noetainflem1 
 |-  ( ( A e. _V /\ B C_ No /\ B e. _V ) -> W e. No )
72 70 68 69 71 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  W e. No )
73 1 2 nosupinfsep 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ W e. No ) -> ( ( A. a e. A a  ( A. a e. A a
74 67 68 69 72 73 syl121anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a  ( A. a e. A a
75 simpr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( dom S u. dom T ) = dom T )
76 75 reseq2d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( W |` ( dom S u. dom T ) ) = ( W |` dom T ) )
77 simplr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( B C_ No /\ B e. _V ) )
78 2 4 noetainflem2 
 |-  ( ( B C_ No /\ B e. _V ) -> ( W |` dom T ) = T )
79 77 78 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( W |` dom T ) = T )
80 76 79 eqtrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( W |` ( dom S u. dom T ) ) = T )
81 80 breq2d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( a  a
82 81 ralbidv 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( A. a e. A a  A. a e. A a
83 80 breq1d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( ( W |` ( dom S u. dom T ) )  T
84 83 ralbidv 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( A. b e. B ( W |` ( dom S u. dom T ) )  A. b e. B T
85 82 84 anbi12d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( dom S u. dom T ) = dom T ) -> ( ( A. a e. A a  ( A. a e. A a
86 85 3adantl3 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a  ( A. a e. A a
87 74 86 bitrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a  ( A. a e. A a
88 66 87 mpbid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( A. a e. A a
89 88 ex 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( dom S u. dom T ) = dom T -> ( A. a e. A a
90 55 89 orim12d 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( ( dom S u. dom T ) = dom S \/ ( dom S u. dom T ) = dom T ) -> ( ( A. a e. A a
91 19 90 mpd 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a
92 91 adantr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( A. a e. A a
93 simpll 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( A C_ No /\ A e. _V ) )
94 simprl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> O e. On )
95 ssun1 
 |-  A C_ ( A u. B )
96 imass2 
 |-  ( A C_ ( A u. B ) -> ( bday " A ) C_ ( bday " ( A u. B ) ) )
97 95 96 ax-mp 
 |-  ( bday " A ) C_ ( bday " ( A u. B ) )
98 simprr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( bday " ( A u. B ) ) C_ O )
99 97 98 sstrid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( bday " A ) C_ O )
100 1 nosupbday 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> ( bday ` S ) C_ O )
101 93 94 99 100 syl12anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( bday ` S ) C_ O )
102 101 a1d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( bday ` S ) C_ O ) )
103 102 ancld 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( ( A. a e. A a
104 df-3an 
 |-  ( ( A. a e. A a  ( ( A. a e. A a
105 103 104 imbitrrdi 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( A. a e. A a
106 93 9 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> S e. No )
107 105 106 jctild 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( S e. No /\ ( A. a e. A a
108 simplr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( B C_ No /\ B e. _V ) )
109 ssun2 
 |-  B C_ ( A u. B )
110 imass2 
 |-  ( B C_ ( A u. B ) -> ( bday " B ) C_ ( bday " ( A u. B ) ) )
111 109 110 ax-mp 
 |-  ( bday " B ) C_ ( bday " ( A u. B ) )
112 111 98 sstrid 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( bday " B ) C_ O )
113 2 noinfbday 
 |-  ( ( ( B C_ No /\ B e. _V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) -> ( bday ` T ) C_ O )
114 108 94 112 113 syl12anc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( bday ` T ) C_ O )
115 114 a1d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( bday ` T ) C_ O ) )
116 115 ancld 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( ( A. a e. A a
117 df-3an 
 |-  ( ( A. a e. A a  ( ( A. a e. A a
118 116 117 imbitrrdi 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( A. a e. A a
119 108 5 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> T e. No )
120 118 119 jctild 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( A. a e. A a  ( T e. No /\ ( A. a e. A a
121 107 120 orim12d 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) ) /\ ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) ) -> ( ( ( A. a e. A a  ( ( S e. No /\ ( A. a e. A a
122 121 3adantl3 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( ( A. a e. A a  ( ( S e. No /\ ( A. a e. A a
123 92 122 mpd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  ( ( S e. No /\ ( A. a e. A a