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 bdayfun ⊢ Fun bday
3 simp1r ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → 𝐴 ∈ 𝑉 )
4 simp2r ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → 𝐵 ∈ 𝑊 )
5 3 4 unexd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
6 funimaexg ⊢ ( ( Fun bday ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
7 2 5 6 sylancr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
8 7 uniexd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
9 imassrn ⊢ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ ran bday
10 bdayrn ⊢ ran bday = On
11 9 10 sseqtri ⊢ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On
12 ssorduni ⊢ ( ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On → Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
13 11 12 ax-mp ⊢ Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) )
14 elon2 ⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ ( Ord ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∧ ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V ) )
15 13 14 mpbiran ⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
16 8 15 sylibr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
17 onsucb ⊢ ( ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ↔ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
18 16 17 sylib ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On )
19 onsucuni ⊢ ( ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ On → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
20 11 19 mp1i ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
21 noeta ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ∧ ( suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) ) → ∃ 𝑧 ∈ No ( ∀ 𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘ 𝑧 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )
22 1 18 20 21 syl12anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → ∃ 𝑧 ∈ No ( ∀ 𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘ 𝑧 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )