Metamath Proof Explorer

Theorem noetalem2

Description: Lemma for noeta . The full statement of the theorem with hypotheses in place. (Contributed by Scott Fenton, 10-Aug-2024)

Ref Expression
Hypotheses noetalem2.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 ) ) ) )
noetalem2.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 ) ) ) )
Assertion noetalem2 
|- ( ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. a e. A A. b e. B a  E. c e. No ( A. a e. A a

Proof

Step Hyp Ref Expression
1 noetalem2.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 noetalem2.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 elex 
 |-  ( A e. V -> A e. _V )
4 3 anim2i 
 |-  ( ( A C_ No /\ A e. V ) -> ( A C_ No /\ A e. _V ) )
5 elex 
 |-  ( B e. W -> B e. _V )
6 5 anim2i 
 |-  ( ( B C_ No /\ B e. W ) -> ( B C_ No /\ B e. _V ) )
7 id 
 |-  ( A. a e. A A. b e. B a  A. a e. A A. b e. B a
8 4 6 7 3anim123i 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. a e. A A. b e. B a  ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a
9 eqid 
 |-  ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) = ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
10 eqid 
 |-  ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
11 1 2 9 10 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
12 breq2 
 |-  ( c = S -> ( a  a
13 12 ralbidv 
 |-  ( c = S -> ( A. a e. A a  A. a e. A a
14 breq1 
 |-  ( c = S -> ( c  S
15 14 ralbidv 
 |-  ( c = S -> ( A. b e. B c  A. b e. B S
16 fveq2 
 |-  ( c = S -> ( bday ` c ) = ( bday ` S ) )
17 16 sseq1d 
 |-  ( c = S -> ( ( bday ` c ) C_ O <-> ( bday ` S ) C_ O ) )
18 13 15 17 3anbi123d 
 |-  ( c = S -> ( ( A. a e. A a  ( A. a e. A a
19 18 rspcev 
 |-  ( ( S e. No /\ ( A. a e. A a  E. c e. No ( A. a e. A a
20 breq2 
 |-  ( c = T -> ( a  a
21 20 ralbidv 
 |-  ( c = T -> ( A. a e. A a  A. a e. A a
22 breq1 
 |-  ( c = T -> ( c  T
23 22 ralbidv 
 |-  ( c = T -> ( A. b e. B c  A. b e. B T
24 fveq2 
 |-  ( c = T -> ( bday ` c ) = ( bday ` T ) )
25 24 sseq1d 
 |-  ( c = T -> ( ( bday ` c ) C_ O <-> ( bday ` T ) C_ O ) )
26 21 23 25 3anbi123d 
 |-  ( c = T -> ( ( A. a e. A a  ( A. a e. A a
27 26 rspcev 
 |-  ( ( T e. No /\ ( A. a e. A a  E. c e. No ( A. a e. A a
28 19 27 jaoi 
 |-  ( ( ( S e. No /\ ( A. a e. A a  E. c e. No ( A. a e. A a
29 11 28 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. a e. A A. b e. B a  E. c e. No ( A. a e. A a
30 8 29 sylan 
 |-  ( ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. a e. A A. b e. B a  E. c e. No ( A. a e. A a