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 27974

Description: Lemma for noeta 27977. 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 789	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ⊆ No )
2		simplrr 790	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ V)
3		simpll 779	. . . . . 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 27965	. . . . 5 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V ∧ 𝑎 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
7	1, 2, 4, 6	syl3anc 1398	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
8		simplll 787	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐴 ⊆ No )
9		simprl 783	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ 𝐴)
10	8, 9	sseldd 3935	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ No )
11		nodmord 27887	. . . . . . . . . 10 ⊢ (𝑎 ∈ No → Ord dom 𝑎)
12		ordirr 6379	. . . . . . . . . 10 ⊢ (Ord dom 𝑎 → ¬ dom 𝑎 ∈ dom 𝑎)
13	10, 11, 12	3syl 19	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 ∈ dom 𝑎)
14		bdayval 27882	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ No → ( bday ‘𝑎) = dom 𝑎)
15	10, 14	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) = dom 𝑎)
16		bdayfo 27911	. . . . . . . . . . . . . . . 16 ⊢ bday : No –onto→On
17		fofn 6795	. . . . . . . . . . . . . . . 16 ⊢ ( bday : No –onto→On → bday Fn No )
18	16, 17	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ bday Fn No
19		fnfvima 7235	. . . . . . . . . . . . . . 15 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑎 ∈ 𝐴) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
20	18, 8, 9, 19	mp3an2i 1495	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
21	15, 20	eqeltrrd 2863	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ ( bday “ 𝐴))
22		elssuni 4902	. . . . . . . . . . . . 13 ⊢ (dom 𝑎 ∈ ( bday “ 𝐴) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
23	21, 22	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
24		nodmon 27884	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ No → dom 𝑎 ∈ On)
25		imassrn 6071	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐴) ⊆ ran bday
26		forn 6796	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
27	16, 26	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
28	25, 27	sseqtri 3982	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐴) ⊆ On
29		ssorduni 7781	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐴) ⊆ On → Ord ∪ ( bday “ 𝐴))
30	28, 29	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐴)
31		ordsssuc 6453	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑎 ∈ On ∧ Ord ∪ ( bday “ 𝐴)) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
32	30, 31	mpan2 704	. . . . . . . . . . . . 13 ⊢ (dom 𝑎 ∈ On → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
33	10, 24, 32	3syl 19	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
34	23, 33	mpbid 235	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ suc ∪ ( bday “ 𝐴))
35		elun2 4132	. . . . . . . . . . 11 ⊢ (dom 𝑎 ∈ suc ∪ ( bday “ 𝐴) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
36	34, 35	syl 18	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
37		eleq2 2851	. . . . . . . . . 10 ⊢ (dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)) → (dom 𝑎 ∈ dom 𝑎 ↔ dom 𝑎 ∈ (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))))
38	36, 37	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)) → dom 𝑎 ∈ dom 𝑎))
39	13, 38	mtod 201	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
40		dmeq 5891	. . . . . . . . 9 ⊢ (𝑎 = 𝑊 → dom 𝑎 = dom 𝑊)
41		noetainflem.2	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
42	41	dmeqi 5892	. . . . . . . . . 10 ⊢ dom 𝑊 = dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
43		dmun 5898	. . . . . . . . . 10 ⊢ dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
44		2oex 8470	. . . . . . . . . . . . . 14 ⊢ 2_o ∈ V
45	44	snnz 4740	. . . . . . . . . . . . 13 ⊢ {2_o} ≠ ∅
46		dmxp 5917	. . . . . . . . . . . . 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 4115	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
49		undif2 4434	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
50	48, 49	eqtri 2785	. . . . . . . . . 10 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
51	42, 43, 50	3eqtri 2789	. . . . . . . . 9 ⊢ dom 𝑊 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
52	40, 51	eqtrdi 2813	. . . . . . . 8 ⊢ (𝑎 = 𝑊 → dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
53	39, 52	nsyl 141	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ 𝑎 = 𝑊)
54	53	neqned 2964	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ≠ 𝑊)
55		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇)
56	10	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ No )
57	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ∈ No )
58		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐴 ∈ V)
59		simplrl 789	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ⊆ No )
60	59	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ⊆ No )
61		simplrr 790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ∈ V)
62	61	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ∈ V)
63	5, 41	noetainflem1 27971	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑊 ∈ No )
64	58, 60, 62, 63	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑊 ∈ No )
65	64	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑊 ∈ No )
66		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ≠ 𝑊)
67		nosepne 27914	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
68	57, 65, 66, 67	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
69	55	fvresd 6902	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
70		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝐵 ⊆ No ∧ 𝐵 ∈ V))
71	5, 41	noetainflem2 27972	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
72	70, 71	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
73	72	fveq1d 6884	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
74	69, 73	eqtr3d 2799	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
75	68, 74	neeqtrd 3026	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
76	75	necomd 3012	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
77		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑇‘𝑞) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
78		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑎‘𝑞) = (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
79	77, 78	neeq12d 3018	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})))
80	79	rspcev 3579	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∧ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
81	55, 76, 80	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
82		df-ne 2958	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
83		fvres 6901	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑎 ↾ dom 𝑇)‘𝑞) = (𝑎‘𝑞))
84	83	neeq2d 3017	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
85	82, 84	bitr3id 288	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ dom 𝑇 → (¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
86	85	rexbiia 3109	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
87		rexnal 3116	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
88	86, 87	bitr3i 280	. . . . . . . . . . . 12 ⊢ (∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
89	81, 88	sylib 221	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
90	89	olcd 888	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
91	5	noinfno 27952	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑇 ∈ No )
92	91	ad3antlr 744	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑇 ∈ No )
93	92	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑇 ∈ No )
94		nofun 27883	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ No → Fun 𝑇)
95	93, 94	syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun 𝑇)
96		nofun 27883	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ No → Fun 𝑎)
97		funres 6579	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑎 → Fun (𝑎 ↾ dom 𝑇))
98	57, 96, 97	3syl 19	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun (𝑎 ↾ dom 𝑇))
99		eqfunfv 7032	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑇 ∧ Fun (𝑎 ↾ dom 𝑇)) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
100	95, 98, 99	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
101		ianor 997	. . . . . . . . . . . . 13 ⊢ (¬ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
102	101	con1bii 359	. . . . . . . . . . . 12 ⊢ (¬ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
103	100, 102	bitr4di 292	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ ¬ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
104	103	con2bid 357	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ ¬ 𝑇 = (𝑎 ↾ dom 𝑇)))
105	90, 104	mpbid 235	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ 𝑇 = (𝑎 ↾ dom 𝑇))
106	105	pm2.21d 122	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊))
107	72	breq2d 5119	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) ↔ (𝑎 ↾ dom 𝑇) <s 𝑇))
108		nodmon 27884	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
109	92, 108	syl 18	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → dom 𝑇 ∈ On)
110	109	adantr 486	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → dom 𝑇 ∈ On)
111		ltsres 27896	. . . . . . . . . 10 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ dom 𝑇 ∈ On) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
112	57, 65, 110, 111	syl3anc 1398	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
113	107, 112	sylbird 263	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s 𝑇 → 𝑎 <s 𝑊))
114		simplrr 790	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
115	114	adantr 486	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
116		noreson 27894	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ No ∧ dom 𝑇 ∈ On) → (𝑎 ↾ dom 𝑇) ∈ No )
117	56, 109, 116	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (𝑎 ↾ dom 𝑇) ∈ No )
118	117	adantr 486	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎 ↾ dom 𝑇) ∈ No )
119		ltsso 27910	. . . . . . . . . . . 12 ⊢ <s Or No
120		sotric 5597	. . . . . . . . . . . 12 ⊢ (( <s Or No ∧ (𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No )) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
121	119, 120	mpan 703	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No ) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
122	93, 118, 121	syl2anc 596	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
123	122	con2bid 357	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇) ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
124	115, 123	mpbird 260	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇))
125	106, 113, 124	mpjaod 874	. . . . . . 7 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 <s 𝑊)
126	64	adantr 486	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ∈ No )
127	56	adantr 486	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ∈ No )
128		simplr 781	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ≠ 𝑊)
129	128	necomd 3012	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ≠ 𝑎)
130	41	fveq1i 6883	. . . . . . . . 9 ⊢ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
131	92	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 ∈ No )
132	131, 94	syl 18	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → Fun 𝑇)
133	132	funfnd 6568	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 Fn dom 𝑇)
134		fnconstg 6767	. . . . . . . . . . . . 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 4429	. . . . . . . . . . . 12 ⊢ (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅)
139		nosepssdm 27920	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎)
140	127, 126, 128, 139	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎)
141	127, 14	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) = dom 𝑎)
142		simp-5l 797	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝐴 ⊆ No )
143		simplrl 789	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ 𝐴)
144	143	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ∈ 𝐴)
145	18, 142, 144, 19	mp3an2i 1495	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
146		elssuni 4902	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑎) ∈ ( bday “ 𝐴) → ( bday ‘𝑎) ⊆ ∪ ( bday “ 𝐴))
147	145, 146	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) ⊆ ∪ ( bday “ 𝐴))
148	141, 147	eqsstrrd 3969	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
149	127, 24, 32	3syl 19	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
150	148, 149	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → dom 𝑎 ∈ suc ∪ ( bday “ 𝐴))
151		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ≠ 𝑊)
152		nosepon 27899	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
153	56, 64, 151, 152	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
154	153	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
155		eloni 6371	. . . . . . . . . . . . . 14 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
156		ordsuc 7813	. . . . . . . . . . . . . . . 16 ⊢ (Ord ∪ ( bday “ 𝐴) ↔ Ord suc ∪ ( bday “ 𝐴))
157	30, 156	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ Ord suc ∪ ( bday “ 𝐴)
158		ordtr2 6407	. . . . . . . . . . . . . . 15 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐴)) → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
159	157, 158	mpan2 704	. . . . . . . . . . . . . 14 ⊢ (Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
160	154, 155, 159	3syl 19	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
161	140, 150, 160	mp2and 712	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴))
162		ontri1 6396	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑇 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇))
163	109, 153, 162	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇))
164	163	biimpa 482	. . . . . . . . . . . 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 6976	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
167	44	fvconst2 7206	. . . . . . . . . . 11 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) → (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
168	165, 167	syl 18	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
169	166, 168	eqtrd 2797	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
170	130, 169	eqtrid 2809	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
171		nosep2o 27916	. . . . . . . 8 ⊢ (((𝑊 ∈ No ∧ 𝑎 ∈ No ∧ 𝑊 ≠ 𝑎) ∧ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o) → 𝑎 <s 𝑊)
172	126, 127, 129, 170, 171	syl31anc 1400	. . . . . . 7 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 <s 𝑊)
173	153, 155	syl 18	. . . . . . . 8 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
174		nodmord 27887	. . . . . . . . 9 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
175	92, 174	syl 18	. . . . . . . 8 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord dom 𝑇)
176		ordtri2or 6462	. . . . . . . 8 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord dom 𝑇) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
177	173, 175, 176	syl2anc 596	. . . . . . 7 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
178	125, 172, 177	mpjaodan 973	. . . . . 6 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 <s 𝑊)
179	54, 178	mpdan 700	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 <s 𝑊)
180	179	expr 462	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (¬ 𝑇 <s (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊))
181	7, 180	sylbid 243	. . 3 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → 𝑎 <s 𝑊))
182	181	ralimdva 3176	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊))
183	182	3impia 1135	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)

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 1570 ∈ wcel 2145 {cab 2740 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 {crab 3414 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 ifcif 4485 {csn 4587 ⟨cop 4593 ∪ cuni 4870 ∩ cint 4910 class class class wbr 5107 ↦ cmpt 5190 Or wor 5566 × cxp 5657 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 Ord word 6360 Oncon0 6361 suc csuc 6363 ℩cio 6491 Fun wfun 6531 Fn wfn 6532 –onto→wfo 6535 ‘cfv 6537 ℩crio 7372 1_oc1o 8451 2_oc2o 8452 No csur 27874 <s clts 27875 bday cbday 27876

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-ord 6364 df-on 6365 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-1o 8458 df-2o 8459 df-no 27877 df-lts 27878 df-bday 27879

This theorem is used by: noetalem1 27975

W3C validator