MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  noetalem1 Structured version   Visualization version   GIF version

Theorem noetalem1 27593
Description: Lemma for noeta 27595. Either 𝑆 or 𝑇 satisfies the final condition. (Contributed by Scott Fenton, 9-Aug-2024.)
Hypotheses
Ref Expression
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
Ref Expression
noetalem1 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((𝑆 No ∧ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏 ∧ ( bday 𝑆) ⊆ 𝑂)) ∨ (𝑇 No ∧ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏 ∧ ( bday 𝑇) ⊆ 𝑂))))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑔   𝑢,𝑎,𝐴,𝑣,𝑥,𝑦   𝐵,𝑎,𝑏,𝑔   𝑢,𝐵   𝑣,𝑏,𝐵,𝑥,𝑦   𝑢,𝑔,𝑣,𝑥,𝑦   𝑢,𝑂,𝑦   𝑆,𝑎,𝑏,𝑔,𝑥   𝑇,𝑎,𝑏,𝑔,𝑥   𝑣,𝑢,𝑥,𝑦   𝑊,𝑎,𝑏,𝑔,𝑥   𝑥,𝑦   𝑍,𝑎,𝑏,𝑔,𝑥
Allowed substitution hints:   𝑆(𝑦,𝑣,𝑢)   𝑇(𝑦,𝑣,𝑢)   𝑂(𝑥,𝑣,𝑔,𝑎,𝑏)   𝑊(𝑦,𝑣,𝑢)   𝑍(𝑦,𝑣,𝑢)

Proof of Theorem noetalem1
StepHypRef Expression
1 noetalem1.2 . . . . . . . . . 10 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21noinfno 27570 . . . . . . . . 9 ((𝐵 No 𝐵 ∈ V) → 𝑇 No )
32adantl 481 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝑇 No )
4 nodmord 27505 . . . . . . . 8 (𝑇 No → Ord dom 𝑇)
53, 4syl 17 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → Ord dom 𝑇)
6 noetalem1.1 . . . . . . . . . 10 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
76nosupno 27555 . . . . . . . . 9 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
87adantr 480 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝑆 No )
9 nodmord 27505 . . . . . . . 8 (𝑆 No → Ord dom 𝑆)
108, 9syl 17 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → Ord dom 𝑆)
11 ordtri2or2 6454 . . . . . . 7 ((Ord dom 𝑇 ∧ Ord dom 𝑆) → (dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇))
125, 10, 11syl2anc 583 . . . . . 6 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇))
13 ssequn2 4176 . . . . . . 7 (dom 𝑇 ⊆ dom 𝑆 ↔ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆)
14 ssequn1 4173 . . . . . . 7 (dom 𝑆 ⊆ dom 𝑇 ↔ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇)
1513, 14orbi12i 911 . . . . . 6 ((dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇) ↔ ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇))
1612, 15sylib 217 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇))
17163adant3 1129 . . . 4 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇))
18 simplll 772 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝐴 No )
19 simpllr 773 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝐴 ∈ V)
20 simplrr 775 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝐵 ∈ V)
21 simpr 484 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝑎𝐴)
22 noetalem1.3 . . . . . . . . . . . . 13 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
236, 22noetasuplem3 27587 . . . . . . . . . . . 12 (((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑎𝐴) → 𝑎 <s 𝑍)
2418, 19, 20, 21, 23syl31anc 1370 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑎𝐴) → 𝑎 <s 𝑍)
2524ralrimiva 3138 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ∀𝑎𝐴 𝑎 <s 𝑍)
26253adant3 1129 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑎𝐴 𝑎 <s 𝑍)
276, 22noetasuplem4 27588 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
2826, 27jca 511 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → (∀𝑎𝐴 𝑎 <s 𝑍 ∧ ∀𝑏𝐵 𝑍 <s 𝑏))
2928adantr 480 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑎𝐴 𝑎 <s 𝑍 ∧ ∀𝑏𝐵 𝑍 <s 𝑏))
30 simp1l 1194 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → 𝐴 No )
31 simp1r 1195 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → 𝐴 ∈ V)
32 simp2r 1197 . . . . . . . . . . 11 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → 𝐵 ∈ V)
336, 22noetasuplem1 27585 . . . . . . . . . . 11 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 No )
3430, 31, 32, 33syl3anc 1368 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → 𝑍 No )
356, 1nosupinfsep 27584 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ 𝑍 No ) → ((∀𝑎𝐴 𝑎 <s 𝑍 ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
3634, 35syld3an3 1406 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ((∀𝑎𝐴 𝑎 <s 𝑍 ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
3736adantr 480 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎𝐴 𝑎 <s 𝑍 ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
38 simpr 484 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (dom 𝑆 ∪ dom 𝑇) = dom 𝑆)
3938reseq2d 5972 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) = (𝑍 ↾ dom 𝑆))
40 simplll 772 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → 𝐴 No )
41 simpllr 773 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → 𝐴 ∈ V)
42 simplrr 775 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → 𝐵 ∈ V)
436, 22noetasuplem2 27586 . . . . . . . . . . . . . 14 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑍 ↾ dom 𝑆) = 𝑆)
4440, 41, 42, 43syl3anc 1368 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
4539, 44eqtrd 2764 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) = 𝑆)
4645breq2d 5151 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ 𝑎 <s 𝑆))
4746ralbidv 3169 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑎𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ∀𝑎𝐴 𝑎 <s 𝑆))
4845breq1d 5149 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏𝑆 <s 𝑏))
4948ralbidv 3169 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑏𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ∀𝑏𝐵 𝑆 <s 𝑏))
5047, 49anbi12d 630 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏)))
51503adantl3 1165 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏)))
5237, 51bitrd 279 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎𝐴 𝑎 <s 𝑍 ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏)))
5329, 52mpbid 231 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏))
5453ex 412 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 → (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏)))
55 noetalem1.4 . . . . . . . . . 10 𝑊 = (𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
561, 55noetainflem4 27592 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑎𝐴 𝑎 <s 𝑊)
57 simpllr 773 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐴 ∈ V)
58 simplrl 774 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐵 No )
59 simplrr 775 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐵 ∈ V)
60 simpr 484 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝑏𝐵)
611, 55noetainflem3 27591 . . . . . . . . . . . 12 (((𝐴 ∈ V ∧ 𝐵 No 𝐵 ∈ V) ∧ 𝑏𝐵) → 𝑊 <s 𝑏)
6257, 58, 59, 60, 61syl31anc 1370 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝑊 <s 𝑏)
6362ralrimiva 3138 . . . . . . . . . 10 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ∀𝑏𝐵 𝑊 <s 𝑏)
64633adant3 1129 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑏𝐵 𝑊 <s 𝑏)
6556, 64jca 511 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → (∀𝑎𝐴 𝑎 <s 𝑊 ∧ ∀𝑏𝐵 𝑊 <s 𝑏))
6665adantr 480 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑎𝐴 𝑎 <s 𝑊 ∧ ∀𝑏𝐵 𝑊 <s 𝑏))
67 simpl1 1188 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝐴 No 𝐴 ∈ V))
68 simpl2l 1223 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝐵 No )
69 simpl2r 1224 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝐵 ∈ V)
70 simpl1r 1222 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝐴 ∈ V)
711, 55noetainflem1 27589 . . . . . . . . . 10 ((𝐴 ∈ V ∧ 𝐵 No 𝐵 ∈ V) → 𝑊 No )
7270, 68, 69, 71syl3anc 1368 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝑊 No )
736, 1nosupinfsep 27584 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ 𝑊 No ) → ((∀𝑎𝐴 𝑎 <s 𝑊 ∧ ∀𝑏𝐵 𝑊 <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
7467, 68, 69, 72, 73syl121anc 1372 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎𝐴 𝑎 <s 𝑊 ∧ ∀𝑏𝐵 𝑊 <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
75 simpr 484 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (dom 𝑆 ∪ dom 𝑇) = dom 𝑇)
7675reseq2d 5972 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) = (𝑊 ↾ dom 𝑇))
77 simplr 766 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝐵 No 𝐵 ∈ V))
781, 55noetainflem2 27590 . . . . . . . . . . . . . 14 ((𝐵 No 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
7977, 78syl 17 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
8076, 79eqtrd 2764 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) = 𝑇)
8180breq2d 5151 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ 𝑎 <s 𝑇))
8281ralbidv 3169 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑎𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ∀𝑎𝐴 𝑎 <s 𝑇))
8380breq1d 5149 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏𝑇 <s 𝑏))
8483ralbidv 3169 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑏𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ∀𝑏𝐵 𝑇 <s 𝑏))
8582, 84anbi12d 630 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)))
86853adantl3 1165 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)))
8774, 86bitrd 279 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎𝐴 𝑎 <s 𝑊 ∧ ∀𝑏𝐵 𝑊 <s 𝑏) ↔ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)))
8866, 87mpbid 231 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏))
8988ex 412 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑇 → (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)))
9054, 89orim12d 961 . . . 4 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → (((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) ∨ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏))))
9117, 90mpd 15 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) ∨ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)))
9291adantr 480 . 2 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) ∨ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)))
93 simpll 764 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → (𝐴 No 𝐴 ∈ V))
94 simprl 768 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → 𝑂 ∈ On)
95 ssun1 4165 . . . . . . . . . . 11 𝐴 ⊆ (𝐴𝐵)
96 imass2 6092 . . . . . . . . . . 11 (𝐴 ⊆ (𝐴𝐵) → ( bday 𝐴) ⊆ ( bday “ (𝐴𝐵)))
9795, 96ax-mp 5 . . . . . . . . . 10 ( bday 𝐴) ⊆ ( bday “ (𝐴𝐵))
98 simprr 770 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ( bday “ (𝐴𝐵)) ⊆ 𝑂)
9997, 98sstrid 3986 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ( bday 𝐴) ⊆ 𝑂)
1006nosupbday 27557 . . . . . . . . 9 (((𝐴 No 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐴) ⊆ 𝑂)) → ( bday 𝑆) ⊆ 𝑂)
10193, 94, 99, 100syl12anc 834 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ( bday 𝑆) ⊆ 𝑂)
102101a1d 25 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) → ( bday 𝑆) ⊆ 𝑂))
103102ancld 550 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) ∧ ( bday 𝑆) ⊆ 𝑂)))
104 df-3an 1086 . . . . . 6 ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏 ∧ ( bday 𝑆) ⊆ 𝑂) ↔ ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) ∧ ( bday 𝑆) ⊆ 𝑂))
105103, 104imbitrrdi 251 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) → (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏 ∧ ( bday 𝑆) ⊆ 𝑂)))
10693, 7syl 17 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → 𝑆 No )
107105, 106jctild 525 . . . 4 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) → (𝑆 No ∧ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏 ∧ ( bday 𝑆) ⊆ 𝑂))))
108 simplr 766 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → (𝐵 No 𝐵 ∈ V))
109 ssun2 4166 . . . . . . . . . . 11 𝐵 ⊆ (𝐴𝐵)
110 imass2 6092 . . . . . . . . . . 11 (𝐵 ⊆ (𝐴𝐵) → ( bday 𝐵) ⊆ ( bday “ (𝐴𝐵)))
111109, 110ax-mp 5 . . . . . . . . . 10 ( bday 𝐵) ⊆ ( bday “ (𝐴𝐵))
112111, 98sstrid 3986 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ( bday 𝐵) ⊆ 𝑂)
1131noinfbday 27572 . . . . . . . . 9 (((𝐵 No 𝐵 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday 𝐵) ⊆ 𝑂)) → ( bday 𝑇) ⊆ 𝑂)
114108, 94, 112, 113syl12anc 834 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ( bday 𝑇) ⊆ 𝑂)
115114a1d 25 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏) → ( bday 𝑇) ⊆ 𝑂))
116115ancld 550 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏) → ((∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏) ∧ ( bday 𝑇) ⊆ 𝑂)))
117 df-3an 1086 . . . . . 6 ((∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏 ∧ ( bday 𝑇) ⊆ 𝑂) ↔ ((∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏) ∧ ( bday 𝑇) ⊆ 𝑂))
118116, 117imbitrrdi 251 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏) → (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏 ∧ ( bday 𝑇) ⊆ 𝑂)))
119108, 2syl 17 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → 𝑇 No )
120118, 119jctild 525 . . . 4 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏) → (𝑇 No ∧ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏 ∧ ( bday 𝑇) ⊆ 𝑂))))
121107, 120orim12d 961 . . 3 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → (((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) ∨ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)) → ((𝑆 No ∧ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏 ∧ ( bday 𝑆) ⊆ 𝑂)) ∨ (𝑇 No ∧ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏 ∧ ( bday 𝑇) ⊆ 𝑂)))))
1221213adantl3 1165 . 2 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → (((∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏) ∨ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏)) → ((𝑆 No ∧ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏 ∧ ( bday 𝑆) ⊆ 𝑂)) ∨ (𝑇 No ∧ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏 ∧ ( bday 𝑇) ⊆ 𝑂)))))
12392, 122mpd 15 1 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ ( bday “ (𝐴𝐵)) ⊆ 𝑂)) → ((𝑆 No ∧ (∀𝑎𝐴 𝑎 <s 𝑆 ∧ ∀𝑏𝐵 𝑆 <s 𝑏 ∧ ( bday 𝑆) ⊆ 𝑂)) ∨ (𝑇 No ∧ (∀𝑎𝐴 𝑎 <s 𝑇 ∧ ∀𝑏𝐵 𝑇 <s 𝑏 ∧ ( bday 𝑇) ⊆ 𝑂))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3a 1084   = wceq 1533  wcel 2098  {cab 2701  wral 3053  wrex 3062  Vcvv 3466  cdif 3938  cun 3939  wss 3941  ifcif 4521  {csn 4621  cop 4627   cuni 4900   class class class wbr 5139  cmpt 5222   × cxp 5665  dom cdm 5667  cres 5669  cima 5670  Ord word 6354  Oncon0 6355  suc csuc 6357  cio 6484  cfv 6534  crio 7357  1oc1o 8455  2oc2o 8456   No csur 27492   <s cslt 27493   bday cbday 27494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-ord 6358  df-on 6359  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-1o 8462  df-2o 8463  df-no 27495  df-slt 27496  df-bday 27497
This theorem is referenced by:  noetalem2  27594
  Copyright terms: Public domain W3C validator