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 27799

Description: Lemma for noeta 27802. 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 3994	. . . . 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 27790	. . . . 5 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V ∧ 𝑎 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
7	1, 2, 4, 6	syl3anc 1370	. . . 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 3995	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ No )
11		nodmord 27712	. . . . . . . . . 10 ⊢ (𝑎 ∈ No → Ord dom 𝑎)
12		ordirr 6403	. . . . . . . . . 10 ⊢ (Ord dom 𝑎 → ¬ dom 𝑎 ∈ dom 𝑎)
13	10, 11, 12	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 ∈ dom 𝑎)
14		bdayval 27707	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ No → ( bday ‘𝑎) = dom 𝑎)
15	10, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) = dom 𝑎)
16		bdayfo 27736	. . . . . . . . . . . . . . . 16 ⊢ bday : No –onto→On
17		fofn 6822	. . . . . . . . . . . . . . . 16 ⊢ ( bday : No –onto→On → bday Fn No )
18	16, 17	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ bday Fn No
19		fnfvima 7252	. . . . . . . . . . . . . . 15 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑎 ∈ 𝐴) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
20	18, 8, 9, 19	mp3an2i 1465	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
21	15, 20	eqeltrrd 2839	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ ( bday “ 𝐴))
22		elssuni 4941	. . . . . . . . . . . . 13 ⊢ (dom 𝑎 ∈ ( bday “ 𝐴) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
24		nodmon 27709	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ No → dom 𝑎 ∈ On)
25		imassrn 6090	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐴) ⊆ ran bday
26		forn 6823	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
27	16, 26	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
28	25, 27	sseqtri 4031	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐴) ⊆ On
29		ssorduni 7797	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐴) ⊆ On → Ord ∪ ( bday “ 𝐴))
30	28, 29	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐴)
31		ordsssuc 6474	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑎 ∈ On ∧ Ord ∪ ( bday “ 𝐴)) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
32	30, 31	mpan2 691	. . . . . . . . . . . . 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 4192	. . . . . . . . . . 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 2827	. . . . . . . . . 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 5916	. . . . . . . . 9 ⊢ (𝑎 = 𝑊 → dom 𝑎 = dom 𝑊)
41		noetainflem.2	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
42	41	dmeqi 5917	. . . . . . . . . 10 ⊢ dom 𝑊 = dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
43		dmun 5923	. . . . . . . . . 10 ⊢ dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))
44		2oex 8515	. . . . . . . . . . . . . 14 ⊢ 2_o ∈ V
45	44	snnz 4780	. . . . . . . . . . . . 13 ⊢ {2_o} ≠ ∅
46		dmxp 5941	. . . . . . . . . . . . 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 4174	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
49		undif2 4482	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
50	48, 49	eqtri 2762	. . . . . . . . . 10 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
51	42, 43, 50	3eqtri 2766	. . . . . . . . 9 ⊢ dom 𝑊 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
52	40, 51	eqtrdi 2790	. . . . . . . 8 ⊢ (𝑎 = 𝑊 → dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
53	39, 52	nsyl 140	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ 𝑎 = 𝑊)
54	53	neqned 2944	. . . . . 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 27796	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑊 ∈ No )
64	58, 60, 62, 63	syl3anc 1370	. . . . . . . . . . . . . . . . 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 27739	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
68	57, 65, 66, 67	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
69	55	fvresd 6926	. . . . . . . . . . . . . . . 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 27797	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
72	70, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
73	72	fveq1d 6908	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
74	69, 73	eqtr3d 2776	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
75	68, 74	neeqtrd 3007	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
76	75	necomd 2993	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
77		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑇‘𝑞) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
78		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑎‘𝑞) = (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
79	77, 78	neeq12d 2999	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})))
80	79	rspcev 3621	. . . . . . . . . . . . 13 ⊢ ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∧ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
81	55, 76, 80	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
82		df-ne 2938	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
83		fvres 6925	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑎 ↾ dom 𝑇)‘𝑞) = (𝑎‘𝑞))
84	83	neeq2d 2998	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
85	82, 84	bitr3id 285	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ dom 𝑇 → (¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
86	85	rexbiia 3089	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
87		rexnal 3097	. . . . . . . . . . . . 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 874	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
91	5	noinfno 27777	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑇 ∈ No )
92	91	ad3antlr 731	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑇 ∈ No )
93	92	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑇 ∈ No )
94		nofun 27708	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ No → Fun 𝑇)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun 𝑇)
96		nofun 27708	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ No → Fun 𝑎)
97		funres 6609	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑎 → Fun (𝑎 ↾ dom 𝑇))
98	57, 96, 97	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun (𝑎 ↾ dom 𝑇))
99		eqfunfv 7055	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑇 ∧ Fun (𝑎 ↾ dom 𝑇)) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
100	95, 98, 99	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ↔ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))))
101		ianor 983	. . . . . . . . . . . . 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 5159	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) ↔ (𝑎 ↾ dom 𝑇) <s 𝑇))
108		nodmon 27709	. . . . . . . . . . . 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 27721	. . . . . . . . . 10 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ dom 𝑇 ∈ On) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) → 𝑎 <s 𝑊))
112	57, 65, 110, 111	syl3anc 1370	. . . . . . . . 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 27719	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ No ∧ dom 𝑇 ∈ On) → (𝑎 ↾ dom 𝑇) ∈ No )
117	56, 109, 116	syl2anc 584	. . . . . . . . . . . 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 27735	. . . . . . . . . . . 12 ⊢ <s Or No
120		sotric 5625	. . . . . . . . . . . 12 ⊢ (( <s Or No ∧ (𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No )) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
121	119, 120	mpan 690	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No ) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
122	93, 118, 121	syl2anc 584	. . . . . . . . . 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 860	. . . . . . 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 2993	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ≠ 𝑎)
130	41	fveq1i 6907	. . . . . . . . 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 6598	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 Fn dom 𝑇)
134		fnconstg 6796	. . . . . . . . . . . . 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 4477	. . . . . . . . . . . 12 ⊢ (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅)
139		nosepssdm 27745	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎)
140	127, 126, 128, 139	syl3anc 1370	. . . . . . . . . . . . 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 1465	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ( bday ‘𝑎) ∈ ( bday “ 𝐴))
146		elssuni 4941	. . . . . . . . . . . . . . . 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 4034	. . . . . . . . . . . . . 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 27724	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
153	56, 64, 151, 152	syl3anc 1370	. . . . . . . . . . . . . . 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 6395	. . . . . . . . . . . . . 14 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
156		ordsuc 7832	. . . . . . . . . . . . . . . 16 ⊢ (Ord ∪ ( bday “ 𝐴) ↔ Ord suc ∪ ( bday “ 𝐴))
157	30, 156	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ Ord suc ∪ ( bday “ 𝐴)
158		ordtr2 6429	. . . . . . . . . . . . . . 15 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐴)) → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
159	157, 158	mpan2 691	. . . . . . . . . . . . . 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 699	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴))
162		ontri1 6419	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑇 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On) → (dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇))
163	109, 153, 162	syl2anc 584	. . . . . . . . . . . . 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 3973	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
166	133, 136, 138, 165	fvun2d 7002	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
167	44	fvconst2 7223	. . . . . . . . . . 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 2774	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2_o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
170	130, 169	eqtrid 2786	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o)
171		nosep2o 27741	. . . . . . . 8 ⊢ (((𝑊 ∈ No ∧ 𝑎 ∈ No ∧ 𝑊 ≠ 𝑎) ∧ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2_o) → 𝑎 <s 𝑊)
172	126, 127, 129, 170, 171	syl31anc 1372	. . . . . . 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 27712	. . . . . . . . 9 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
175	92, 174	syl 17	. . . . . . . 8 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord dom 𝑇)
176		ordtri2or 6483	. . . . . . . 8 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord dom 𝑇) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
177	173, 175, 176	syl2anc 584	. . . . . . 7 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇 ∨ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
178	125, 172, 177	mpjaodan 960	. . . . . 6 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 <s 𝑊)
179	54, 178	mpdan 687	. . . . 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 3164	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊))
183	182	3impia 1116	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1536 ∈ wcel 2105 {cab 2711 ≠ wne 2937 ∀wral 3058 ∃wrex 3067 {crab 3432 Vcvv 3477 ∖ cdif 3959 ∪ cun 3960 ∩ cin 3961 ⊆ wss 3962 ∅c0 4338 ifcif 4530 {csn 4630 ⟨cop 4636 ∪ cuni 4911 ∩ cint 4950 class class class wbr 5147 ↦ cmpt 5230 Or wor 5595 × cxp 5686 dom cdm 5688 ran crn 5689 ↾ cres 5690 “ cima 5691 Ord word 6384 Oncon0 6385 suc csuc 6387 ℩cio 6513 Fun wfun 6556 Fn wfn 6557 –onto→wfo 6560 ‘cfv 6562 ℩crio 7386 1_oc1o 8497 2_oc2o 8498 No csur 27698 <s cslt 27699 bday cbday 27700

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4912 df-int 4951 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-ord 6388 df-on 6389 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-1o 8504 df-2o 8505 df-no 27701 df-slt 27702 df-bday 27703

This theorem is referenced by: noetalem1 27800

W3C validator