Metamath Proof Explorer

Theorem noeta2

Description: A version of noeta with fewer hypotheses but a weaker upper bound (Contributed by Scott Fenton, 7-Dec-2021)

Ref Expression
Assertion noeta2 
|- ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  E. z e. No ( A. x e. A x

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x
2 bdayfo 
 |-  bday : No -onto-> On
3 fofun 
 |-  ( bday : No -onto-> On -> Fun bday )
4 2 3 ax-mp 
 |-  Fun bday
5 simp1r 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  A e. V )
6 simp2r 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  B e. W )
7 unexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
8 5 6 7 syl2anc 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  ( A u. B ) e. _V )
9 funimaexg 
 |-  ( ( Fun bday /\ ( A u. B ) e. _V ) -> ( bday " ( A u. B ) ) e. _V )
10 4 8 9 sylancr 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  ( bday " ( A u. B ) ) e. _V )
11 10 uniexd 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  U. ( bday " ( A u. B ) ) e. _V )
12 imassrn 
 |-  ( bday " ( A u. B ) ) C_ ran bday
13 forn 
 |-  ( bday : No -onto-> On -> ran bday = On )
14 2 13 ax-mp 
 |-  ran bday = On
15 12 14 sseqtri 
 |-  ( bday " ( A u. B ) ) C_ On
16 ssorduni 
 |-  ( ( bday " ( A u. B ) ) C_ On -> Ord U. ( bday " ( A u. B ) ) )
17 15 16 ax-mp 
 |-  Ord U. ( bday " ( A u. B ) )
18 elon2 
 |-  ( U. ( bday " ( A u. B ) ) e. On <-> ( Ord U. ( bday " ( A u. B ) ) /\ U. ( bday " ( A u. B ) ) e. _V ) )
19 17 18 mpbiran 
 |-  ( U. ( bday " ( A u. B ) ) e. On <-> U. ( bday " ( A u. B ) ) e. _V )
20 11 19 sylibr 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  U. ( bday " ( A u. B ) ) e. On )
21 sucelon 
 |-  ( U. ( bday " ( A u. B ) ) e. On <-> suc U. ( bday " ( A u. B ) ) e. On )
22 20 21 sylib 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  suc U. ( bday " ( A u. B ) ) e. On )
23 onsucuni 
 |-  ( ( bday " ( A u. B ) ) C_ On -> ( bday " ( A u. B ) ) C_ suc U. ( bday " ( A u. B ) ) )
24 15 23 mp1i 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  ( bday " ( A u. B ) ) C_ suc U. ( bday " ( A u. B ) ) )
25 noeta 
 |-  ( ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  E. z e. No ( A. x e. A x
26 1 22 24 25 syl12anc 
 |-  ( ( ( A C_ No /\ A e. V ) /\ ( B C_ No /\ B e. W ) /\ A. x e. A A. y e. B x  E. z e. No ( A. x e. A x