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 ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ∃ 𝑧 ∈ No ( ∀ 𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘ 𝑧 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) )
2 bdayfo ⊢ bday : No –onto→ On
3 fofun ⊢ ( bday : No –onto→ On → Fun bday )
4 2 3 ax-mp ⊢ Fun bday
5 simp1r ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → 𝐴 ∈ 𝑉 )
6 simp2r ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → 𝐵 ∈ 𝑊 )
7 unexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
8 5 6 7 syl2anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
9 funimaexg ⊢ ( ( Fun bday ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
10 4 8 9 sylancr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
11 10 uniexd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
12 imassrn ⊢ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ ran bday
13 forn ⊢ ( bday : No –onto→ On → ran bday = On )
14 2 13 ax-mp ⊢ ran bday = On
15 12 14 sseqtri ⊢ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On
16 ssorduni ⊢ ( ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On → Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
17 15 16 ax-mp ⊢ Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) )
18 elon2 ⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ ( Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∧ ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V ) )
19 17 18 mpbiran ⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
20 11 19 sylibr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
21 sucelon ⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
22 20 21 sylib ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
23 onsucuni ⊢ ( ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
24 15 23 mp1i ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
25 noeta ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ∧ ( suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) → ∃ 𝑧 ∈ No ( ∀ 𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘ 𝑧 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )
26 1 22 24 25 syl12anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ∃ 𝑧 ∈ No ( ∀ 𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘ 𝑧 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )