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 27803

Description: Lemma for noeta 27806. 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 776	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ⊆ No )
2		simplrr 777	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ V)
3		simpll 766	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝐴 ⊆ No )
4	3	sselda 4008	. . . . 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 27794	. . . . 5 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V ∧ 𝑎 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
7	1, 2, 4, 6	syl3anc 1371	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
8		simplll 774	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐴 ⊆ No )
9		simprl 770	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ 𝐴)
10	8, 9	sseldd 4009	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ No )
11		nodmord 27716	. . . . . . . . . 10 ⊢ (𝑎 ∈ No → Ord dom 𝑎)
12		ordirr 6413	. . . . . . . . . 10 ⊢ (Ord dom 𝑎 → ¬ dom 𝑎 ∈ dom 𝑎)
13	10, 11, 12	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 ∈ dom 𝑎)
14		bdayval 27711	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ No → ( bday ‘𝑎) = dom 𝑎)
15	10, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) = dom 𝑎)
16		bdayfo 27740	. . . . . . . . . . . . . . . 16 ⊢ bday : No –onto→On
17		fofn 6836	. . . . . . . . . . . . . . . 16 ⊢ ( bday : No –onto→On → bday Fn No )
18	16, 17	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ bday Fn No
19		fnfvima 7270	. . . . . . . . . . . . . . 15 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑎 ∈ 𝐴) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
20	18, 8, 9, 19	mp3an2i 1466	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
21	15, 20	eqeltrrd 2845	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ ( bday “ 𝐴))
22		elssuni 4961	. . . . . . . . . . . . 13 ⊢ (dom 𝑎 ∈ ( bday “ 𝐴) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
24		nodmon 27713	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ No → dom 𝑎 ∈ On)
25		imassrn 6100	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐴) ⊆ ran bday
26		forn 6837	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
27	16, 26	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
28	25, 27	sseqtri 4045	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐴) ⊆ On
29		ssorduni 7814	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐴) ⊆ On → Ord ∪ ( bday “ 𝐴))
30	28, 29	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐴)
31		ordsssuc 6484	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑎 ∈ On ∧ Ord ∪ ( bday “ 𝐴)) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
32	30, 31	mpan2 690	. . . . . . . . . . . . 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 4206	. . . . . . . . . . 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 2833	. . . . . . . . . 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 5928	. . . . . . . . 9 ⊢ (𝑎 = 𝑊 → dom 𝑎 = dom 𝑊)
41		noetainflem.2	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
42	41	dmeqi 5929	. . . . . . . . . 10 ⊢ dom 𝑊 = dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
43		dmun 5935	. . . . . . . . . 10 ⊢ dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
44		2oex 8533	. . . . . . . . . . . . . 14 ⊢ 2_o ∈ V
45	44	snnz 4801	. . . . . . . . . . . . 13 ⊢ {2_o} ≠ ∅
46		dmxp 5953	. . . . . . . . . . . . 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 4188	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
49		undif2 4500	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
50	48, 49	eqtri 2768	. . . . . . . . . 10 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
51	42, 43, 50	3eqtri 2772	. . . . . . . . 9 ⊢ dom 𝑊 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
52	40, 51	eqtrdi 2796	. . . . . . . 8 ⊢ (𝑎 = 𝑊 → dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
53	39, 52	nsyl 140	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ 𝑎 = 𝑊)
54	53	neqned 2953	. . . . . 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 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐴 ∈ V)
59		simplrl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ⊆ No )
60	59	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ⊆ No )
61		simplrr 777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ∈ V)
62	61	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ∈ V)
63	5, 41	noetainflem1 27800	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑊 ∈ No )
64	58, 60, 62, 63	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑊 ∈ No )
65	64	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑊 ∈ No )
66		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ≠ 𝑊)
67		nosepne 27743	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
68	57, 65, 66, 67	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
69	55	fvresd 6940	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
70		simp-4r 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝐵 ⊆ No ∧ 𝐵 ∈ V))
71	5, 41	noetainflem2 27801	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
72	70, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
73	72	fveq1d 6922	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
74	69, 73	eqtr3d 2782	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
75	68, 74	neeqtrd 3016	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
76	75	necomd 3002	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
77		fveq2 6920	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑇‘𝑞) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
78		fveq2 6920	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑎‘𝑞) = (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
79	77, 78	neeq12d 3008	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})))
80	79	rspcev 3635	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∧ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
81	55, 76, 80	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
82		df-ne 2947	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
83		fvres 6939	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑎 ↾ dom 𝑇)‘𝑞) = (𝑎‘𝑞))
84	83	neeq2d 3007	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
85	82, 84	bitr3id 285	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ dom 𝑇 → (¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
86	85	rexbiia 3098	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
87		rexnal 3106	. . . . . . . . . . . . 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 873	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
91	5	noinfno 27781	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑇 ∈ No )
92	91	ad3antlr 730	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑇 ∈ No )
93	92	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑇 ∈ No )
94		nofun 27712	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ No → Fun 𝑇)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun 𝑇)
96		nofun 27712	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ No → Fun 𝑎)
97		funres 6620	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑎 → Fun (𝑎 ↾ dom 𝑇))
98	57, 96, 97	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun (𝑎 ↾ dom 𝑇))
99		eqfunfv 7069	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑇 ∧ Fun (𝑎 ↾ dom 𝑇)) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
100	95, 98, 99	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
101		ianor 982	. . . . . . . . . . . . 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 5178	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) ↔ (𝑎 ↾ dom 𝑇) <s 𝑇))
108		nodmon 27713	. . . . . . . . . . . 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		sltres 27725	. . . . . . . . . 10 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ dom 𝑇 ∈ On) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
112	57, 65, 110, 111	syl3anc 1371	. . . . . . . . 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 777	. . . . . . . . . 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 27723	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ No ∧ dom 𝑇 ∈ On) → (𝑎 ↾ dom 𝑇) ∈ No )
117	56, 109, 116	syl2anc 583	. . . . . . . . . . . 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		sltso 27739	. . . . . . . . . . . 12 ⊢ <s Or No
120		sotric 5637	. . . . . . . . . . . 12 ⊢ (( <s Or No ∧ (𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No )) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
121	119, 120	mpan 689	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No ) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
122	93, 118, 121	syl2anc 583	. . . . . . . . . 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 859	. . . . . . 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 768	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ≠ 𝑊)
129	128	necomd 3002	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ≠ 𝑎)
130	41	fveq1i 6921	. . . . . . . . 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 6609	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 Fn dom 𝑇)
134		fnconstg 6809	. . . . . . . . . . . . 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 4495	. . . . . . . . . . . 12 ⊢ (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅)
139		nosepssdm 27749	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎)
140	127, 126, 128, 139	syl3anc 1371	. . . . . . . . . . . . 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 784	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝐴 ⊆ No )
143		simplrl 776	. . . . . . . . . . . . . . . . . 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 1466	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
146		elssuni 4961	. . . . . . . . . . . . . . . 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 4048	. . . . . . . . . . . . . 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 27728	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
153	56, 64, 151, 152	syl3anc 1371	. . . . . . . . . . . . . . 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 6405	. . . . . . . . . . . . . 14 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
156		ordsuc 7849	. . . . . . . . . . . . . . . 16 ⊢ (Ord ∪ ( bday “ 𝐴) ↔ Ord suc ∪ ( bday “ 𝐴))
157	30, 156	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ Ord suc ∪ ( bday “ 𝐴)
158		ordtr2 6439	. . . . . . . . . . . . . . 15 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐴)) → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
159	157, 158	mpan2 690	. . . . . . . . . . . . . 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 698	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴))
162		ontri1 6429	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑇 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇))
163	109, 153, 162	syl2anc 583	. . . . . . . . . . . . 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 3987	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
166	133, 136, 138, 165	fvun2d 7016	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
167	44	fvconst2 7241	. . . . . . . . . . 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 2780	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
170	130, 169	eqtrid 2792	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
171		nosep2o 27745	. . . . . . . 8 ⊢ (((𝑊 ∈ No ∧ 𝑎 ∈ No ∧ 𝑊 ≠ 𝑎) ∧ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o) → 𝑎 <s 𝑊)
172	126, 127, 129, 170, 171	syl31anc 1373	. . . . . . 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 27716	. . . . . . . . 9 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
175	92, 174	syl 17	. . . . . . . 8 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord dom 𝑇)
176		ordtri2or 6493	. . . . . . . 8 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord dom 𝑇) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
177	173, 175, 176	syl2anc 583	. . . . . . 7 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
178	125, 172, 177	mpjaodan 959	. . . . . 6 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 <s 𝑊)
179	54, 178	mpdan 686	. . . . 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 3173	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊))
183	182	3impia 1117	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 {cab 2717 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 {crab 3443 Vcvv 3488 ∖ cdif 3973 ∪ cun 3974 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 ifcif 4548 {csn 4648 ⟨cop 4654 ∪ cuni 4931 ∩ cint 4970 class class class wbr 5166 ↦ cmpt 5249 Or wor 5606 × cxp 5698 dom cdm 5700 ran crn 5701 ↾ cres 5702 “ cima 5703 Ord word 6394 Oncon0 6395 suc csuc 6397 ℩cio 6523 Fun wfun 6567 Fn wfn 6568 –onto→wfo 6571 ‘cfv 6573 ℩crio 7403 1_oc1o 8515 2_oc2o 8516 No csur 27702 <s cslt 27703 bday cbday 27704

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-ord 6398 df-on 6399 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-1o 8522 df-2o 8523 df-no 27705 df-slt 27706 df-bday 27707

This theorem is referenced by: noetalem1 27804

W3C validator