Metamath Proof Explorer

Theorem noetalem1

Description: Lemma for noeta . Either S or T satisfies the final condition. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetalem1.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
noetalem1.2 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
noetalem1.3 ⊢ 𝑍 = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
noetalem1.4 ⊢ 𝑊 = ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
Assertion noetalem1 ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) ∨ ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) ) )

Proof

Step Hyp Ref Expression
1 noetalem1.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 noetalem1.2 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
3 noetalem1.3 ⊢ 𝑍 = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
4 noetalem1.4 ⊢ 𝑊 = ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
5 2 noinfno ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑇 ∈ No )
6 5 adantl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → 𝑇 ∈ No )
7 nodmord ⊢ ( 𝑇 ∈ No → Ord dom 𝑇 )
8 6 7 syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → Ord dom 𝑇 )
9 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
10 9 adantr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → 𝑆 ∈ No )
11 nodmord ⊢ ( 𝑆 ∈ No → Ord dom 𝑆 )
12 10 11 syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → Ord dom 𝑆 )
13 ordtri2or2 ⊢ ( ( Ord dom 𝑇 ∧ Ord dom 𝑆 ) → ( dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇 ) )
14 8 12 13 syl2anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ( dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇 ) )
15 ssequn2 ⊢ ( dom 𝑇 ⊆ dom 𝑆 ↔ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 )
16 ssequn1 ⊢ ( dom 𝑆 ⊆ dom 𝑇 ↔ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 )
17 15 16 orbi12i ⊢ ( ( dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇 ) ↔ ( ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ∨ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) )
18 14 17 sylib ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ( ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ∨ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) )
19 18 3adant3 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ∨ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) )
20 simplll ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐴 ⊆ No )
21 simpllr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐴 ∈ V )
22 simplrr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐵 ∈ V )
23 simpr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
24 1 3 noetasuplem3 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s 𝑍 )
25 20 21 22 23 24 syl31anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s 𝑍 )
26 25 ralrimiva ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 )
27 26 3adant3 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 )
28 1 3 noetasuplem4 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 )
29 27 28 jca ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) )
30 29 adantr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) )
31 simp1l ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → 𝐴 ⊆ No )
32 simp1r ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → 𝐴 ∈ V )
33 simp2r ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → 𝐵 ∈ V )
34 1 3 noetasuplem1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑍 ∈ No )
35 31 32 33 34 syl3anc ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → 𝑍 ∈ No )
36 1 2 nosupinfsep ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑍 ∈ No ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ) )
37 35 36 syld3an3 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ) )
38 37 adantr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ) )
39 simpr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 )
40 39 reseq2d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) = ( 𝑍 ↾ dom 𝑆 ) )
41 simplll ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → 𝐴 ⊆ No )
42 simpllr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → 𝐴 ∈ V )
43 simplrr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → 𝐵 ∈ V )
44 1 3 noetasuplem2 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )
45 41 42 43 44 syl3anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )
46 40 45 eqtrd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) = 𝑆 )
47 46 breq2d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( 𝑎 <s ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↔ 𝑎 <s 𝑆 ) )
48 47 ralbidv ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↔ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ) )
49 46 breq1d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ↔ 𝑆 <s 𝑏 ) )
50 49 ralbidv ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ∀ 𝑏 ∈ 𝐵 ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) )
51 48 50 anbi12d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ) )
52 51 3adantl3 ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑍 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ) )
53 38 52 bitrd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ) )
54 30 53 mpbid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) )
55 54 ex ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ) )
56 2 4 noetainflem4 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑊 )
57 simpllr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ V )
58 simplrl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ⊆ No )
59 simplrr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ∈ V )
60 simpr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
61 2 4 noetainflem3 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑏 ∈ 𝐵 ) → 𝑊 <s 𝑏 )
62 57 58 59 60 61 syl31anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑊 <s 𝑏 )
63 62 ralrimiva ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) → ∀ 𝑏 ∈ 𝐵 𝑊 <s 𝑏 )
64 63 3adant3 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ∀ 𝑏 ∈ 𝐵 𝑊 <s 𝑏 )
65 56 64 jca ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏 ∈ 𝐵 𝑊 <s 𝑏 ) )
66 65 adantr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏 ∈ 𝐵 𝑊 <s 𝑏 ) )
67 simpl1 ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
68 simpl2l ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → 𝐵 ⊆ No )
69 simpl2r ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → 𝐵 ∈ V )
70 simpl1r ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → 𝐴 ∈ V )
71 2 4 noetainflem1 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑊 ∈ No )
72 70 68 69 71 syl3anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → 𝑊 ∈ No )
73 1 2 nosupinfsep ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ 𝑊 ∈ No ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏 ∈ 𝐵 𝑊 <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ) )
74 67 68 69 72 73 syl121anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏 ∈ 𝐵 𝑊 <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ) )
75 simpr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 )
76 75 reseq2d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) = ( 𝑊 ↾ dom 𝑇 ) )
77 simplr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) )
78 2 4 noetainflem2 ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( 𝑊 ↾ dom 𝑇 ) = 𝑇 )
79 77 78 syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( 𝑊 ↾ dom 𝑇 ) = 𝑇 )
80 76 79 eqtrd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) = 𝑇 )
81 80 breq2d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↔ 𝑎 <s 𝑇 ) )
82 81 ralbidv ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↔ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ) )
83 80 breq1d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ↔ 𝑇 <s 𝑏 ) )
84 83 ralbidv ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ∀ 𝑏 ∈ 𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) )
85 82 84 anbi12d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) )
86 85 3adantl3 ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) )
87 74 86 bitrd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏 ∈ 𝐵 𝑊 <s 𝑏 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) )
88 66 87 mpbid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) )
89 88 ex ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) )
90 55 89 orim12d ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ( ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑆 ∨ ( dom 𝑆 ∪ dom 𝑇 ) = dom 𝑇 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ∨ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) ) )
91 19 90 mpd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ∨ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) )
92 91 adantr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ∨ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) )
93 simpll ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
94 simprl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → 𝑂 ∈ On )
95 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
96 imass2 ⊢ ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → ( bday “ 𝐴 ) ⊆ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
97 95 96 ax-mp ⊢ ( bday “ 𝐴 ) ⊆ ( bday “ ( 𝐴 ∪ 𝐵 ) )
98 simprr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 )
99 97 98 sstrid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( bday “ 𝐴 ) ⊆ 𝑂 )
100 1 nosupbday ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) → ( bday ‘ 𝑆 ) ⊆ 𝑂 )
101 93 94 99 100 syl12anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( bday ‘ 𝑆 ) ⊆ 𝑂 )
102 101 a1d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) → ( bday ‘ 𝑆 ) ⊆ 𝑂 ) )
103 102 ancld ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) )
104 df-3an ⊢ ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ↔ ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) )
105 103 104 imbitrrdi ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) )
106 93 9 syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → 𝑆 ∈ No )
107 105 106 jctild ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) → ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) ) )
108 simplr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) )
109 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
110 imass2 ⊢ ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) → ( bday “ 𝐵 ) ⊆ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
111 109 110 ax-mp ⊢ ( bday “ 𝐵 ) ⊆ ( bday “ ( 𝐴 ∪ 𝐵 ) )
112 111 98 sstrid ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( bday “ 𝐵 ) ⊆ 𝑂 )
113 2 noinfbday ⊢ ( ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐵 ) ⊆ 𝑂 ) ) → ( bday ‘ 𝑇 ) ⊆ 𝑂 )
114 108 94 112 113 syl12anc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( bday ‘ 𝑇 ) ⊆ 𝑂 )
115 114 a1d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) → ( bday ‘ 𝑇 ) ⊆ 𝑂 ) )
116 115 ancld ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) )
117 df-3an ⊢ ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ↔ ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) )
118 116 117 imbitrrdi ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) )
119 108 5 syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → 𝑇 ∈ No )
120 118 119 jctild ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) → ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) ) )
121 107 120 orim12d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ∨ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) → ( ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) ∨ ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) ) ) )
122 121 3adantl3 ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) ∨ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) ) → ( ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) ∨ ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) ) ) )
123 92 122 mpd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) ∨ ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) ) )