noetalem1 - Metamath Proof Explorer

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

Theorem noetalem1 28098

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

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

**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**
Step	Hyp	Ref	Expression
1		noetalem1.2	. . . . . . . . . 10 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2	1	noinfno 28075	. . . . . . . . 9 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑇 ∈ No)
3	2	adantl 487	. . . . . . . 8 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝑇 ∈ No)
4		nodmord 28010	. . . . . . . 8 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
5	3, 4	syl 18	. . . . . . 7 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → Ord dom 𝑇)
6		noetalem1.1	. . . . . . . . . 10 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
7	6	nosupno 28060	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No)
8	7	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝑆 ∈ No)
9		nodmord 28010	. . . . . . . 8 ⊢ (𝑆 ∈ No → Ord dom 𝑆)
10	8, 9	syl 18	. . . . . . 7 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → Ord dom 𝑆)
11		ordtri2or2 6464	. . . . . . 7 ⊢ ((Ord dom 𝑇 ∧ Ord dom 𝑆) → (dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇))
12	5, 10, 11	syl2anc 596	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇))
13		ssequn2 4187	. . . . . . 7 ⊢ (dom 𝑇 ⊆ dom 𝑆 ↔ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆)
14		ssequn1 4184	. . . . . . 7 ⊢ (dom 𝑆 ⊆ dom 𝑇 ↔ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇)
15	13, 14	orbi12i 928	. . . . . 6 ⊢ ((dom 𝑇 ⊆ dom 𝑆 ∨ dom 𝑆 ⊆ dom 𝑇) ↔ ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇))
16	12, 15	sylib 221	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇))
17	16	3adant3 1150	. . . 4 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇))
18		simplll 787	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐴 ⊆ No)
19		simpllr 788	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐴 ∈ V)
20		simplrr 790	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ V)
21		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴)
22		noetalem1.3	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ (bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
23	6, 22	noetasuplem3 28092	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑍)
24	18, 19, 20, 21, 23	syl31anc 1400	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑍)
25	24	ralrimiva 3154	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)
26	25	3adant3 1150	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)
27	6, 22	noetasuplem4 28093	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
28	26, 27	jca 521	. . . . . . . 8 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
29	28	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
30		simp1l 1216	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝐴 ⊆ No)
31		simp1r 1217	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝐴 ∈ V)
32		simp2r 1219	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝐵 ∈ V)
33	6, 22	noetasuplem1 28090	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 ∈ No)
34	30, 31, 32, 33	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝑍 ∈ No)
35	6, 1	nosupinfsep 28089	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑍 ∈ No) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
36	34, 35	syld3an3 1436	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
37	36	adantr 486	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
38		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (dom 𝑆 ∪ dom 𝑇) = dom 𝑆)
39	38	reseq2d 5969	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) = (𝑍 ↾ dom 𝑆))
40		simplll 787	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → 𝐴 ⊆ No)
41		simpllr 788	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → 𝐴 ∈ V)
42		simplrr 790	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → 𝐵 ∈ V)
43	6, 22	noetasuplem2 28091	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑍 ↾ dom 𝑆) = 𝑆)
44	40, 41, 42, 43	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
45	39, 44	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) = 𝑆)
46	45	breq2d 5114	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ 𝑎 <s 𝑆))
47	46	ralbidv 3185	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑎 ∈ 𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑆))
48	45	breq1d 5112	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ 𝑆 <s 𝑏))
49	48	ralbidv 3185	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑏 ∈ 𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏))
50	47, 49	anbi12d 644	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎 ∈ 𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏)))
51	50	3adantl3 1187	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎 ∈ 𝐴 𝑎 <s (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑍 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏)))
52	37, 51	bitrd 282	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏)))
53	29, 52	mpbid 235	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑆) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏))
54	53	ex 418	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏)))
55		noetalem1.4	. . . . . . . . . 10 ⊢ 𝑊 = (𝑇 ∪ ((suc ∪ (bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
56	1, 55	noetainflem4 28097	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)
57		simpllr 788	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ V)
58		simplrl 789	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐵 ⊆ No)
59		simplrr 790	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ V)
60		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
61	1, 55	noetainflem3 28096	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑏 ∈ 𝐵) → 𝑊 <s 𝑏)
62	57, 58, 59, 60, 61	syl31anc 1400	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝑊 <s 𝑏)
63	62	ralrimiva 3154	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏)
64	63	3adant3 1150	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏)
65	56, 64	jca 521	. . . . . . . 8 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏))
66	65	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏))
67		simpl1 1210	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
68		simpl2l 1245	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝐵 ⊆ No)
69		simpl2r 1246	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝐵 ∈ V)
70		simpl1r 1244	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝐴 ∈ V)
71	1, 55	noetainflem1 28094	. . . . . . . . . 10 ⊢ ((𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑊 ∈ No)
72	70, 68, 69, 71	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → 𝑊 ∈ No)
73	6, 1	nosupinfsep 28089	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
74	67, 68, 69, 72, 73	syl121anc 1402	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏)))
75		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (dom 𝑆 ∪ dom 𝑇) = dom 𝑇)
76	75	reseq2d 5969	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) = (𝑊 ↾ dom 𝑇))
77		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝐵 ⊆ No ∧ 𝐵 ∈ V))
78	1, 55	noetainflem2 28095	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
79	77, 78	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
80	76, 79	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) = 𝑇)
81	80	breq2d 5114	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ 𝑎 <s 𝑇))
82	81	ralbidv 3185	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑎 ∈ 𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑇))
83	80	breq1d 5112	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ 𝑇 <s 𝑏))
84	83	ralbidv 3185	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏))
85	82, 84	anbi12d 644	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎 ∈ 𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)))
86	85	3adantl3 1187	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎 ∈ 𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)))
87	74, 86	bitrd 282	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)))
88	66, 87	mpbid 235	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏))
89	88	ex 418	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ((dom 𝑆 ∪ dom 𝑇) = dom 𝑇 → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)))
90	54, 89	orim12d 979	. . . 4 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → (((dom 𝑆 ∪ dom 𝑇) = dom 𝑆 ∨ (dom 𝑆 ∪ dom 𝑇) = dom 𝑇) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) ∨ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏))))
91	17, 90	mpd 16	. . 3 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) ∨ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)))
92	91	adantr 486	. 2 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) ∨ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)))
93		simpll 779	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
94		simprl 783	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → 𝑂 ∈ On)
95		ssun1 4176	. . . . . . . . . . 11 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
96		imass2 6054	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ (𝐴 ∪ 𝐵) → (bday “ 𝐴) ⊆ (bday “ (𝐴 ∪ 𝐵)))
97	95, 96	ax-mp 5	. . . . . . . . . 10 ⊢ (bday “ 𝐴) ⊆ (bday “ (𝐴 ∪ 𝐵))
98		simprr 785	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)
99	97, 98	sstrid 3919	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (bday “ 𝐴) ⊆ 𝑂)
100	6	nosupbday 28062	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ (bday “ 𝐴) ⊆ 𝑂)) → (bday‘𝑆) ⊆ 𝑂)
101	93, 94, 99, 100	syl12anc 850	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (bday‘𝑆) ⊆ 𝑂)
102	101	a1d 26	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) → (bday‘𝑆) ⊆ 𝑂))
103	102	ancld 560	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) ∧ (bday‘𝑆) ⊆ 𝑂)))
104		df-3an 1105	. . . . . 6 ⊢ ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ (bday‘𝑆) ⊆ 𝑂) ↔ ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) ∧ (bday‘𝑆) ⊆ 𝑂))
105	103, 104	imbitrrdi 255	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ (bday‘𝑆) ⊆ 𝑂)))
106	93, 7	syl 18	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → 𝑆 ∈ No)
107	105, 106	jctild 535	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) → (𝑆 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ (bday‘𝑆) ⊆ 𝑂))))
108		simplr 781	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (𝐵 ⊆ No ∧ 𝐵 ∈ V))
109		ssun2 4177	. . . . . . . . . . 11 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
110		imass2 6054	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ (𝐴 ∪ 𝐵) → (bday “ 𝐵) ⊆ (bday “ (𝐴 ∪ 𝐵)))
111	109, 110	ax-mp 5	. . . . . . . . . 10 ⊢ (bday “ 𝐵) ⊆ (bday “ (𝐴 ∪ 𝐵))
112	111, 98	sstrid 3919	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (bday “ 𝐵) ⊆ 𝑂)
113	1	noinfbday 28077	. . . . . . . . 9 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ (𝑂 ∈ On ∧ (bday “ 𝐵) ⊆ 𝑂)) → (bday‘𝑇) ⊆ 𝑂)
114	108, 94, 112, 113	syl12anc 850	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (bday‘𝑇) ⊆ 𝑂)
115	114	a1d 26	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏) → (bday‘𝑇) ⊆ 𝑂))
116	115	ancld 560	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏) ∧ (bday‘𝑇) ⊆ 𝑂)))
117		df-3an 1105	. . . . . 6 ⊢ ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ (bday‘𝑇) ⊆ 𝑂) ↔ ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏) ∧ (bday‘𝑇) ⊆ 𝑂))
118	116, 117	imbitrrdi 255	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ (bday‘𝑇) ⊆ 𝑂)))
119	108, 2	syl 18	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → 𝑇 ∈ No)
120	118, 119	jctild 535	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏) → (𝑇 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ (bday‘𝑇) ⊆ 𝑂))))
121	107, 120	orim12d 979	. . 3 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) ∨ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)) → ((𝑆 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ (bday‘𝑆) ⊆ 𝑂)) ∨ (𝑇 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ (bday‘𝑇) ⊆ 𝑂)))))
122	121	3adantl3 1187	. 2 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → (((∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏) ∨ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏)) → ((𝑆 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ (bday‘𝑆) ⊆ 𝑂)) ∨ (𝑇 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ (bday‘𝑇) ⊆ 𝑂)))))
123	92, 122	mpd 16	1 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) ∧ (𝑂 ∈ On ∧ (bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂)) → ((𝑆 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ (bday‘𝑆) ⊆ 𝑂)) ∨ (𝑇 ∈ No ∧ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ (bday‘𝑇) ⊆ 𝑂))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 {cab 2738 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∪ cun 4149 ifcif 4481 {csn 4583 ⟨cop 4589 ∪ cuni 4866 class class class wbr 5102 ↦ cmpt 5185 × cxp 5648 dom cdm 5650 ↾ cres 5652 “ cima 5653 Ord word 6361 Oncon0 6362 suc csuc 6364 ℩cio 6492 ‘cfv 6538 ℩crio 7376 1_oc1o 8469 2_oc2o 8470 Nocsur 27997 <s clts 27998 bdaycbday 27999

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-ord 6365 df-on 6366 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-1o 8476 df-2o 8477 df-no 28000 df-lts 28001 df-bday 28002

This theorem is used by: noetalem2 28099

W3C validator