Theorem noetainflem4 33943

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

Hypotheses

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

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 774	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ⊆ No )
2		simplrr 775	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ V)
3		simpll 764	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝐴 ⊆ No )
4	3	sselda 3921	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No )
5		noetainflem.1	. . . . . 6 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
6	5	noinfbnd2 33934	. . . . 5 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V ∧ 𝑎 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
7	1, 2, 4, 6	syl3anc 1370	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
8		simplll 772	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐴 ⊆ No )
9		simprl 768	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ 𝐴)
10	8, 9	sseldd 3922	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ∈ No )
11		nodmord 33856	. . . . . . . . . 10 ⊢ (𝑎 ∈ No → Ord dom 𝑎)
12		ordirr 6284	. . . . . . . . . 10 ⊢ (Ord dom 𝑎 → ¬ dom 𝑎 ∈ dom 𝑎)
13	10, 11, 12	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 ∈ dom 𝑎)
14		bdayval 33851	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ No → ( bday ‘𝑎) = dom 𝑎)
15	10, 14	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ( bday ‘𝑎) = dom 𝑎)
16		bdayfo 33880	. . . . . . . . . . . . . . . 16 ⊢ bday : No –onto→On
17		fofn 6690	. . . . . . . . . . . . . . . 16 ⊢ ( bday : No –onto→On → bday Fn No )
18	16, 17	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ bday Fn No
19		fnfvima 7109	. . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ ( bday “ 𝐴))
22		elssuni 4871	. . . . . . . . . . . . 13 ⊢ (dom 𝑎 ∈ ( bday “ 𝐴) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ⊆ ∪ ( bday “ 𝐴))
24		nodmon 33853	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ No → dom 𝑎 ∈ On)
25		imassrn 5980	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐴) ⊆ ran bday
26		forn 6691	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
27	16, 26	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
28	25, 27	sseqtri 3957	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐴) ⊆ On
29		ssorduni 7629	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐴) ⊆ On → Ord ∪ ( bday “ 𝐴))
30	28, 29	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐴)
31		ordsssuc 6352	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑎 ∈ On ∧ Ord ∪ ( bday “ 𝐴)) → (dom 𝑎 ⊆ ∪ ( bday “ 𝐴) ↔ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)))
32	30, 31	mpan2 688	. . . . . . . . . . . . 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 231	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → dom 𝑎 ∈ suc ∪ ( bday “ 𝐴))
35		elun2 4111	. . . . . . . . . . 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 246	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → (dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)) → dom 𝑎 ∈ dom 𝑎))
39	13, 38	mtod 197	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
40		dmeq 5812	. . . . . . . . 9 ⊢ (𝑎 = 𝑊 → dom 𝑎 = dom 𝑊)
41		noetainflem.2	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}))
42	41	dmeqi 5813	. . . . . . . . . 10 ⊢ dom 𝑊 = dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}))
43		dmun 5819	. . . . . . . . . 10 ⊢ dom (𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}))
44		2oex 8308	. . . . . . . . . . . . . 14 ⊢ 2o ∈ V
45	44	snnz 4712	. . . . . . . . . . . . 13 ⊢ {2o} ≠ ∅
46		dmxp 5838	. . . . . . . . . . . . 13 ⊢ ({2o} ≠ ∅ → dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) = (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
47	45, 46	ax-mp 5	. . . . . . . . . . . 12 ⊢ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) = (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)
48	47	uneq2i 4094	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
49		undif2 4410	. . . . . . . . . . 11 ⊢ (dom 𝑇 ∪ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
50	48, 49	eqtri 2766	. . . . . . . . . 10 ⊢ (dom 𝑇 ∪ dom ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
51	42, 43, 50	3eqtri 2770	. . . . . . . . 9 ⊢ dom 𝑊 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴))
52	40, 51	eqtrdi 2794	. . . . . . . 8 ⊢ (𝑎 = 𝑊 → dom 𝑎 = (dom 𝑇 ∪ suc ∪ ( bday “ 𝐴)))
53	39, 52	nsyl 140	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → ¬ 𝑎 = 𝑊)
54	53	neqned 2950	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 ≠ 𝑊)
55		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇)
56	10	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ No )
57	56	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ∈ No )
58		simp-4r 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐴 ∈ V)
59		simplrl 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ⊆ No )
60	59	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ⊆ No )
61		simplrr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝐵 ∈ V)
62	61	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝐵 ∈ V)
63	5, 41	noetainflem1 33940	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑊 ∈ No )
64	58, 60, 62, 63	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑊 ∈ No )
65	64	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑊 ∈ No )
66		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 ≠ 𝑊)
67		nosepne 33883	. . . . . . . . . . . . . . . 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 6794	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
70		simp-4r 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝐵 ⊆ No ∧ 𝐵 ∈ V))
71	5, 41	noetainflem2 33941	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
72	70, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊 ↾ dom 𝑇) = 𝑇)
73	72	fveq1d 6776	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑊 ↾ dom 𝑇)‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
74	69, 73	eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
75	68, 74	neeqtrd 3013	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
76	75	necomd 2999	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
77		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑇‘𝑞) = (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
78		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → (𝑎‘𝑞) = (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
79	77, 78	neeq12d 3005	. . . . . . . . . . . . . 14 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} → ((𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ (𝑇‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) ≠ (𝑎‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})))
80	79	rspcev 3561	. . . . . . . . . . . . 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 2944	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
83		fvres 6793	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑎 ↾ dom 𝑇)‘𝑞) = (𝑎‘𝑞))
84	83	neeq2d 3004	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ dom 𝑇 → ((𝑇‘𝑞) ≠ ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
85	82, 84	bitr3id 285	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ dom 𝑇 → (¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ (𝑇‘𝑞) ≠ (𝑎‘𝑞)))
86	85	rexbiia 3180	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞))
87		rexnal 3169	. . . . . . . . . . . . 13 ⊢ (∃𝑞 ∈ dom 𝑇 ¬ (𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
88	86, 87	bitr3i 276	. . . . . . . . . . . 12 ⊢ (∃𝑞 ∈ dom 𝑇(𝑇‘𝑞) ≠ (𝑎‘𝑞) ↔ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
89	81, 88	sylib 217	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞))
90	89	olcd 871	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
91	5	noinfno 33921	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ V) → 𝑇 ∈ No )
92	91	ad3antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑇 ∈ No )
93	92	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑇 ∈ No )
94		nofun 33852	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ No → Fun 𝑇)
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun 𝑇)
96		nofun 33852	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ No → Fun 𝑎)
97		funres 6476	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑎 → Fun (𝑎 ↾ dom 𝑇))
98	57, 96, 97	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → Fun (𝑎 ↾ dom 𝑇))
99		eqfunfv 6914	. . . . . . . . . . . . 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 979	. . . . . . . . . . . . 13 ⊢ (¬ (dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∧ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ (¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)))
102	101	con1bii 357	. . . . . . . . . . . 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 355	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((¬ dom 𝑇 = dom (𝑎 ↾ dom 𝑇) ∨ ¬ ∀𝑞 ∈ dom 𝑇(𝑇‘𝑞) = ((𝑎 ↾ dom 𝑇)‘𝑞)) ↔ ¬ 𝑇 = (𝑎 ↾ dom 𝑇)))
105	90, 104	mpbid 231	. . . . . . . . 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 5086	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s (𝑊 ↾ dom 𝑇) ↔ (𝑎 ↾ dom 𝑇) <s 𝑇))
108		nodmon 33853	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
109	92, 108	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → dom 𝑇 ∈ On)
110	109	adantr 481	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → dom 𝑇 ∈ On)
111		sltres 33865	. . . . . . . . . 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 259	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑎 ↾ dom 𝑇) <s 𝑇 → 𝑎 <s 𝑊))
114		simplrr 775	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
115	114	adantr 481	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))
116		noreson 33863	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ No ∧ dom 𝑇 ∈ On) → (𝑎 ↾ dom 𝑇) ∈ No )
117	56, 109, 116	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → (𝑎 ↾ dom 𝑇) ∈ No )
118	117	adantr 481	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑎 ↾ dom 𝑇) ∈ No )
119		sltso 33879	. . . . . . . . . . . 12 ⊢ <s Or No
120		sotric 5531	. . . . . . . . . . . 12 ⊢ (( <s Or No ∧ (𝑇 ∈ No ∧ (𝑎 ↾ dom 𝑇) ∈ No )) → (𝑇 <s (𝑎 ↾ dom 𝑇) ↔ ¬ (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇)))
121	119, 120	mpan 687	. . . . . . . . . . 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 355	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → ((𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇) ↔ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇)))
124	115, 123	mpbird 256	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → (𝑇 = (𝑎 ↾ dom 𝑇) ∨ (𝑎 ↾ dom 𝑇) <s 𝑇))
125	106, 113, 124	mpjaod 857	. . . . . . 7 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇) → 𝑎 <s 𝑊)
126	64	adantr 481	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ∈ No )
127	56	adantr 481	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ∈ No )
128		simplr 766	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑎 ≠ 𝑊)
129	128	necomd 2999	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑊 ≠ 𝑎)
130	41	fveq1i 6775	. . . . . . . . 9 ⊢ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
131	92	adantr 481	. . . . . . . . . . . . 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 6465	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝑇 Fn dom 𝑇)
134		fnconstg 6662	. . . . . . . . . . . . 13 ⊢ (2o ∈ V → ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
135	44, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)
136	135	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}) Fn (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
137		disjdif 4405	. . . . . . . . . . . 12 ⊢ (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (dom 𝑇 ∩ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇)) = ∅)
139		nosepssdm 33889	. . . . . . . . . . . . . 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 782	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → 𝐴 ⊆ No )
143		simplrl 774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ∈ 𝐴)
144	143	adantr 481	. . . . . . . . . . . . . . . . 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 4871	. . . . . . . . . . . . . . . 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 3960	. . . . . . . . . . . . . 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 231	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → dom 𝑎 ∈ suc ∪ ( bday “ 𝐴))
151		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 ≠ 𝑊)
152		nosepon 33868	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ No ∧ 𝑊 ∈ No ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
153	56, 64, 151, 152	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
154	153	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On)
155		eloni 6276	. . . . . . . . . . . . . 14 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)})
156		ordsuc 7661	. . . . . . . . . . . . . . . 16 ⊢ (Ord ∪ ( bday “ 𝐴) ↔ Ord suc ∪ ( bday “ 𝐴))
157	30, 156	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ Ord suc ∪ ( bday “ 𝐴)
158		ordtr2 6310	. . . . . . . . . . . . . . 15 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐴)) → ((∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ⊆ dom 𝑎 ∧ dom 𝑎 ∈ suc ∪ ( bday “ 𝐴)) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴)))
159	157, 158	mpan2 688	. . . . . . . . . . . . . 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 696	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ suc ∪ ( bday “ 𝐴))
162		ontri1 6300	. . . . . . . . . . . . . 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 477	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ¬ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ dom 𝑇)
165	161, 164	eldifd 3898	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇))
166	133, 136, 138, 165	fvun2d 6862	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}))
167	44	fvconst2 7079	. . . . . . . . . . 11 ⊢ (∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)} ∈ (suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) → (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o)
168	165, 167	syl 17	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o})‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o)
169	166, 168	eqtrd 2778	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → ((𝑇 ∪ ((suc ∪ ( bday “ 𝐴) ∖ dom 𝑇) × {2o}))‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o)
170	130, 169	eqtrid 2790	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) ∧ dom 𝑇 ⊆ ∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) → (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o)
171		nosep2o 33885	. . . . . . . 8 ⊢ (((𝑊 ∈ No ∧ 𝑎 ∈ No ∧ 𝑊 ≠ 𝑎) ∧ (𝑊‘∩ {𝑝 ∈ On ∣ (𝑎‘𝑝) ≠ (𝑊‘𝑝)}) = 2o) → 𝑎 <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 33856	. . . . . . . . 9 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
175	92, 174	syl 17	. . . . . . . 8 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → Ord dom 𝑇)
176		ordtri2or 6361	. . . . . . . 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 956	. . . . . 6 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) ∧ 𝑎 ≠ 𝑊) → 𝑎 <s 𝑊)
179	54, 178	mpdan 684	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑎 ∈ 𝐴 ∧ ¬ 𝑇 <s (𝑎 ↾ dom 𝑇))) → 𝑎 <s 𝑊)
180	179	expr 457	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (¬ 𝑇 <s (𝑎 ↾ dom 𝑇) → 𝑎 <s 𝑊))
181	7, 180	sylbid 239	. . 3 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → (∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → 𝑎 <s 𝑊))
182	181	ralimdva 3108	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊))
183	182	3impia 1116	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  {cab 2715   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  {crab 3068  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ifcif 4459  {csn 4561  ⟨cop 4567  ∪ cuni 4839  ∩ cint 4879   class class class wbr 5074   ↦ cmpt 5157   Or wor 5502   × cxp 5587  dom cdm 5589  ran crn 5590   ↾ cres 5591   “ cima 5592  Ord word 6265  Oncon0 6266  suc csuc 6268  ℩cio 6389  Fun wfun 6427   Fn wfn 6428  –onto→wfo 6431  ‘cfv 6433  ℩crio 7231  1_oc1o 8290  2_oc2o 8291   No csur 33843   <s cslt 33844   bday cbday 33845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-1o 8297  df-2o 8298  df-no 33846  df-slt 33847  df-bday 33848

This theorem is referenced by:  noetalem1  33944