noetainflem4 - Metamath Proof Explorer

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

Theorem noetainflem4 27712

Description: Lemma for noeta 27715. If 𝐴 precedes 𝐵, then 𝑊 is greater than 𝐴. (Contributed by Scott Fenton, 9-Aug-2024.)

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

**Assertion**
Ref	Expression
noetainflem4	⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)

Distinct variable groups: 𝐵,𝑔,𝑢,𝑣,𝑥,𝑦 𝐴,𝑎 𝑎,𝑏,𝑔,𝑥,𝐵 𝑣,𝑏,𝑥,𝑦 𝑇,𝑏,𝑔 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑣,𝑢,𝑔,𝑏) 𝑇(𝑥,𝑦,𝑣,𝑢,𝑎) 𝑊(𝑥,𝑦,𝑣,𝑢,𝑔,𝑎,𝑏)

Proof of Theorem noetainflem4 Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplrl 777	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ⊆ No )
2		simplrr 778	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ V)
3		simpll 767	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝐴 ⊆ No )
4	3	sselda 3934	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No )
5		noetainflem.1	. . . . . 6 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
6	5	noinfbnd2 27703	. . . . 5 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V ∧ 𝑎 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
7	1, 2, 4, 6	syl3anc 1374	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
8		simplll 775	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐴 ⊆ No )
9		simprl 771	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ 𝐴)
10	8, 9	sseldd 3935	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ No )
11		nodmord 27625	. . . . . . . . . 10 ⊢ (𝑎 ∈ No → Ord dom 𝑎)
12		ordirr 6336	. . . . . . . . . 10 ⊢ (Ord dom 𝑎 → ¬ dom 𝑎 ∈ dom 𝑎)
13	10, 11, 12	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 ∈ dom 𝑎)
14		bdayval 27620	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ No → ( bday ‘𝑎) = dom 𝑎)
15	10, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) = dom 𝑎)
16		bdayfo 27649	. . . . . . . . . . . . . . . 16 ⊢ bday : No –onto→On
17		fofn 6749	. . . . . . . . . . . . . . . 16 ⊢ ( bday : No –onto→On → bday Fn No )
18	16, 17	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ bday Fn No
19		fnfvima 7181	. . . . . . . . . . . . . . 15 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑎 ∈ 𝐴) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
20	18, 8, 9, 19	mp3an2i 1469	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
21	15, 20	eqeltrrd 2838	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ ( bday “ 𝐴))
22		elssuni 4895	. . . . . . . . . . . . 13 ⊢ (dom 𝑎 ∈ ( bday “ 𝐴) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
24		nodmon 27622	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ No → dom 𝑎 ∈ On)
25		imassrn 6031	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐴) ⊆ ran bday
26		forn 6750	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
27	16, 26	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
28	25, 27	sseqtri 3983	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐴) ⊆ On
29		ssorduni 7726	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐴) ⊆ On → Ord ∪ ( bday “ 𝐴))
30	28, 29	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐴)
31		ordsssuc 6409	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑎 ∈ On ∧ Ord ∪ ( bday “ 𝐴)) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
32	30, 31	mpan2 692	. . . . . . . . . . . . 13 ⊢ (dom 𝑎 ∈ On → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
33	10, 24, 32	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
34	23, 33	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ suc ∪ ( bday “ 𝐴))
35		elun2 4136	. . . . . . . . . . 11 ⊢ (dom 𝑎 ∈ suc ∪ ( bday “ 𝐴) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
37		eleq2 2826	. . . . . . . . . 10 ⊢ (dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)) → (dom 𝑎 ∈ dom 𝑎 ↔ dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))))
38	36, 37	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)) → dom 𝑎 ∈ dom 𝑎))
39	13, 38	mtod 198	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
40		dmeq 5853	. . . . . . . . 9 ⊢ (𝑎 = 𝑊 → dom 𝑎 = dom 𝑊)
41		noetainflem.2	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
42	41	dmeqi 5854	. . . . . . . . . 10 ⊢ dom 𝑊 = dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
43		dmun 5860	. . . . . . . . . 10 ⊢ dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
44		2oex 8410	. . . . . . . . . . . . . 14 ⊢ 2_o ∈ V
45	44	snnz 4734	. . . . . . . . . . . . 13 ⊢ {2_o} ≠ ∅
46		dmxp 5879	. . . . . . . . . . . . 13 ⊢ ({2_o} ≠ ∅ → dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}) = (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
47	45, 46	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}) = (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)
48	47	uneq2i 4118	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
49		undif2 4430	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
50	48, 49	eqtri 2760	. . . . . . . . . 10 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
51	42, 43, 50	3eqtri 2764	. . . . . . . . 9 ⊢ dom 𝑊 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
52	40, 51	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑎 = 𝑊 → dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
53	39, 52	nsyl 140	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ 𝑎 = 𝑊)
54	53	neqned 2940	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ≠ 𝑊)
55		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇)
56	10	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ No )
57	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ∈ No )
58		simp-4r 784	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐴 ∈ V)
59		simplrl 777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ⊆ No )
60	59	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ⊆ No )
61		simplrr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ∈ V)
62	61	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ∈ V)
63	5, 41	noetainflem1 27709	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑊 ∈ No )
64	58, 60, 62, 63	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑊 ∈ No )
65	64	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑊 ∈ No )
66		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ≠ 𝑊)
67		nosepne 27652	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
68	57, 65, 66, 67	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
69	55	fvresd 6855	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
70		simp-4r 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝐵 ⊆ No ∧ 𝐵 ∈ V))
71	5, 41	noetainflem2 27710	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
72	70, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
73	72	fveq1d 6837	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
74	69, 73	eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
75	68, 74	neeqtrd 3002	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
76	75	necomd 2988	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
77		fveq2 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑇‘𝑞) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
78		fveq2 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑎‘𝑞) = (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
79	77, 78	neeq12d 2994	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})))
80	79	rspcev 3577	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∧ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
81	55, 76, 80	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
82		df-ne 2934	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
83		fvres 6854	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑎 ↾ dom 𝑇)‘𝑞) = (𝑎‘𝑞))
84	83	neeq2d 2993	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
85	82, 84	bitr3id 285	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ dom 𝑇 → (¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
86	85	rexbiia 3082	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
87		rexnal 3089	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
88	86, 87	bitr3i 277	. . . . . . . . . . . 12 ⊢ (∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
89	81, 88	sylib 218	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
90	89	olcd 875	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
91	5	noinfno 27690	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑇 ∈ No )
92	91	ad3antlr 732	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑇 ∈ No )
93	92	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑇 ∈ No )
94		nofun 27621	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ No → Fun 𝑇)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun 𝑇)
96		nofun 27621	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ No → Fun 𝑎)
97		funres 6535	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑎 → Fun (𝑎 ↾ dom 𝑇))
98	57, 96, 97	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun (𝑎 ↾ dom 𝑇))
99		eqfunfv 6983	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑇 ∧ Fun (𝑎 ↾ dom 𝑇)) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
100	95, 98, 99	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
101		ianor 984	. . . . . . . . . . . . 13 ⊢ (¬ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
102	101	con1bii 356	. . . . . . . . . . . 12 ⊢ (¬ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
103	100, 102	bitr4di 289	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ ¬ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
104	103	con2bid 354	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ ¬ 𝑇 = (𝑎 ↾ dom 𝑇)))
105	90, 104	mpbid 232	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ 𝑇 = (𝑎 ↾ dom 𝑇))
106	105	pm2.21d 121	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊))
107	72	breq2d 5111	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) ↔ (𝑎 ↾ dom 𝑇) <s 𝑇))
108		nodmon 27622	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
109	92, 108	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → dom 𝑇 ∈ On)
110	109	adantr 480	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → dom 𝑇 ∈ On)
111		ltsres 27634	. . . . . . . . . 10 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ dom 𝑇 ∈ On) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
112	57, 65, 110, 111	syl3anc 1374	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
113	107, 112	sylbird 260	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s 𝑇 → 𝑎 <s 𝑊))
114		simplrr 778	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
115	114	adantr 480	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
116		noreson 27632	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ No ∧ dom 𝑇 ∈ On) → (𝑎 ↾ dom 𝑇) ∈ No )
117	56, 109, 116	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (𝑎 ↾ dom 𝑇) ∈ No )
118	117	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎 ↾ dom 𝑇) ∈ No )
119		ltsso 27648	. . . . . . . . . . . 12 ⊢ <s Or No
120		sotric 5563	. . . . . . . . . . . 12 ⊢ (( <s Or No ∧ (𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No )) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
121	119, 120	mpan 691	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No ) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
122	93, 118, 121	syl2anc 585	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
123	122	con2bid 354	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇) ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
124	115, 123	mpbird 257	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇))
125	106, 113, 124	mpjaod 861	. . . . . . 7 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 <s 𝑊)
126	64	adantr 480	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ∈ No )
127	56	adantr 480	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ∈ No )
128		simplr 769	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ≠ 𝑊)
129	128	necomd 2988	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ≠ 𝑎)
130	41	fveq1i 6836	. . . . . . . . 9 ⊢ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
131	92	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 ∈ No )
132	131, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → Fun 𝑇)
133	132	funfnd 6524	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 Fn dom 𝑇)
134		fnconstg 6723	. . . . . . . . . . . . 13 ⊢ (2_o ∈ V → ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
135	44, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)
136	135	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
137		disjdif 4425	. . . . . . . . . . . 12 ⊢ (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅)
139		nosepssdm 27658	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎)
140	127, 126, 128, 139	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎)
141	127, 14	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) = dom 𝑎)
142		simp-5l 785	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝐴 ⊆ No )
143		simplrl 777	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ 𝐴)
144	143	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ∈ 𝐴)
145	18, 142, 144, 19	mp3an2i 1469	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
146		elssuni 4895	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑎) ∈ ( bday “ 𝐴) → ( bday ‘𝑎) ⊆ ∪ ( bday “ 𝐴))
147	145, 146	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) ⊆ ∪ ( bday “ 𝐴))
148	141, 147	eqsstrrd 3970	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
149	127, 24, 32	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
150	148, 149	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → dom 𝑎 ∈ suc ∪ ( bday “ 𝐴))
151		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ≠ 𝑊)
152		nosepon 27637	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
153	56, 64, 151, 152	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
154	153	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
155		eloni 6328	. . . . . . . . . . . . . 14 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
156		ordsuc 7758	. . . . . . . . . . . . . . . 16 ⊢ (Ord ∪ ( bday “ 𝐴) ↔ Ord suc ∪ ( bday “ 𝐴))
157	30, 156	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ Ord suc ∪ ( bday “ 𝐴)
158		ordtr2 6363	. . . . . . . . . . . . . . 15 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐴)) → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
159	157, 158	mpan2 692	. . . . . . . . . . . . . 14 ⊢ (Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
160	154, 155, 159	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
161	140, 150, 160	mp2and 700	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴))
162		ontri1 6352	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑇 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇))
163	109, 153, 162	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇))
164	163	biimpa 476	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇)
165	161, 164	eldifd 3913	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
166	133, 136, 138, 165	fvun2d 6929	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
167	44	fvconst2 7152	. . . . . . . . . . 11 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) → (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
168	165, 167	syl 17	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
169	166, 168	eqtrd 2772	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
170	130, 169	eqtrid 2784	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
171		nosep2o 27654	. . . . . . . 8 ⊢ (((𝑊 ∈ No ∧ 𝑎 ∈ No ∧ 𝑊 ≠ 𝑎) ∧ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o) → 𝑎 <s 𝑊)
172	126, 127, 129, 170, 171	syl31anc 1376	. . . . . . 7 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 <s 𝑊)
173	153, 155	syl 17	. . . . . . . 8 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
174		nodmord 27625	. . . . . . . . 9 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
175	92, 174	syl 17	. . . . . . . 8 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord dom 𝑇)
176		ordtri2or 6418	. . . . . . . 8 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord dom 𝑇) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
177	173, 175, 176	syl2anc 585	. . . . . . 7 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
178	125, 172, 177	mpjaodan 961	. . . . . 6 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 <s 𝑊)
179	54, 178	mpdan 688	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 <s 𝑊)
180	179	expr 456	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (¬ 𝑇 <s (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊))
181	7, 180	sylbid 240	. . 3 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → 𝑎 <s 𝑊))
182	181	ralimdva 3149	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊))
183	182	3impia 1118	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 {cab 2715 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 {crab 3400 Vcvv 3441 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4286 ifcif 4480 {csn 4581 ⟨cop 4587 ∪ cuni 4864 ∩ cint 4903 class class class wbr 5099 ↦ cmpt 5180 Or wor 5532 × cxp 5623 dom cdm 5625 ran crn 5626 ↾ cres 5627 “ cima 5628 Ord word 6317 Oncon0 6318 suc csuc 6320 ℩cio 6447 Fun wfun 6487 Fn wfn 6488 –onto→wfo 6491 ‘cfv 6493 ℩crio 7316 1_oc1o 8392 2_oc2o 8393 No csur 27611 <s clts 27612 bday cbday 27613

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4904 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-ord 6321 df-on 6322 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7317 df-1o 8399 df-2o 8400 df-no 27614 df-lts 27615 df-bday 27616

This theorem is referenced by: noetalem1 27713

W3C validator