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 bdayfun 
 |-  Fun bday
3 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 )
4 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 )
5 3 4 unexd 
 |-  ( ( ( 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 )
6 funimaexg 
 |-  ( ( Fun bday /\ ( A u. B ) e. _V ) -> ( bday " ( A u. B ) ) e. _V )
7 2 5 6 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 )
8 7 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 )
9 imassrn 
 |-  ( bday " ( A u. B ) ) C_ ran bday
10 bdayrn 
 |-  ran bday = On
11 9 10 sseqtri 
 |-  ( bday " ( A u. B ) ) C_ On
12 ssorduni 
 |-  ( ( bday " ( A u. B ) ) C_ On -> Ord U. ( bday " ( A u. B ) ) )
13 11 12 ax-mp 
 |-  Ord U. ( bday " ( A u. B ) )
14 elon2 
 |-  ( U. ( bday " ( A u. B ) ) e. On <-> ( Ord U. ( bday " ( A u. B ) ) /\ U. ( bday " ( A u. B ) ) e. _V ) )
15 13 14 mpbiran 
 |-  ( U. ( bday " ( A u. B ) ) e. On <-> U. ( bday " ( A u. B ) ) e. _V )
16 8 15 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 )
17 onsucb 
 |-  ( U. ( bday " ( A u. B ) ) e. On <-> suc U. ( bday " ( A u. B ) ) e. On )
18 16 17 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 )
19 onsucuni 
 |-  ( ( bday " ( A u. B ) ) C_ On -> ( bday " ( A u. B ) ) C_ suc U. ( bday " ( A u. B ) ) )
20 11 19 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 ) ) )
21 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
22 1 18 20 21 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