noetasuplem4 - Metamath Proof Explorer

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

Theorem noetasuplem4 27688

Description: Lemma for noeta 27695. When 𝐴 and 𝐵 are separated, then 𝑍 is a lower bound for 𝐵. Part of Theorem 5.1 of [Lipparini] p. 7-8. (Contributed by Scott Fenton, 7-Dec-2021.)

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

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

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

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

Step	Hyp	Ref	Expression
1		ralcom 3263	. . 3 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ∀𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 𝑎 <s 𝑏)
2		simplll 775	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ⊆ No )
3		simpllr 776	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ V)
4		simprl 771	. . . . . . 7 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝐵 ⊆ No )
5	4	sselda 3917	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
6		noetasuplem.1	. . . . . . 7 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
7	6	nosupbnd2 27668	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑏 ∈ No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
8	2, 3, 5, 7	syl3anc 1374	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
9		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) → 𝑏 ∈ 𝐵)
10		ssel2 3912	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
11	4, 9, 10	syl2an 597	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 ∈ No )
12		nodmord 27605	. . . . . . . . . 10 ⊢ (𝑏 ∈ No → Ord dom 𝑏)
13		ordirr 6330	. . . . . . . . . 10 ⊢ (Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏)
14	11, 12, 13	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏)
15		ssun2 4110	. . . . . . . . . . 11 ⊢ suc ∪ ( bday “ 𝐵) ⊆ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
16		bdayval 27600	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ No → ( bday ‘𝑏) = dom 𝑏)
17	11, 16	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday ‘𝑏) = dom 𝑏)
18		bdayfo 27629	. . . . . . . . . . . . . . . . 17 ⊢ bday : No –onto→On
19		fofn 6743	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → bday Fn No )
20	18, 19	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ bday Fn No
21		fnfvima 7177	. . . . . . . . . . . . . . . 16 ⊢ (( bday Fn No ∧ 𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
22	20, 21	mp3an1 1451	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
23	4, 9, 22	syl2an 597	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
24	17, 23	eqeltrrd 2836	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday “ 𝐵))
25		elssuni 4871	. . . . . . . . . . . . 13 ⊢ (dom 𝑏 ∈ ( bday “ 𝐵) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
27		nodmon 27602	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ No → dom 𝑏 ∈ On)
28		imassrn 6025	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐵) ⊆ ran bday
29		forn 6744	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
30	18, 29	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
31	28, 30	sseqtri 3965	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐵) ⊆ On
32		ssorduni 7722	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐵) ⊆ On → Ord ∪ ( bday “ 𝐵))
33	31, 32	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐵)
34		ordsssuc 6403	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑏 ∈ On ∧ Ord ∪ ( bday “ 𝐵)) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)))
35	33, 34	mpan2 692	. . . . . . . . . . . . 13 ⊢ (dom 𝑏 ∈ On → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)))
36	11, 27, 35	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)))
37	26, 36	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ suc ∪ ( bday “ 𝐵))
38	15, 37	sselid 3915	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)))
39		eleq2 2824	. . . . . . . . . 10 ⊢ ((dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏 → (dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) ↔ dom 𝑏 ∈ dom 𝑏))
40	38, 39	syl5ibcom 245	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ((dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏 → dom 𝑏 ∈ dom 𝑏))
41	14, 40	mtod 198	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏)
42		noetasuplem.2	. . . . . . . . . . . 12 ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
43	42	dmeqi 5848	. . . . . . . . . . 11 ⊢ dom 𝑍 = dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
44		dmun 5854	. . . . . . . . . . 11 ⊢ dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
45	43, 44	eqtri 2758	. . . . . . . . . 10 ⊢ dom 𝑍 = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
46		1oex 8404	. . . . . . . . . . . . 13 ⊢ 1_o ∈ V
47	46	snnz 4710	. . . . . . . . . . . 12 ⊢ {1_o} ≠ ∅
48		dmxp 5873	. . . . . . . . . . . 12 ⊢ ({1_o} ≠ ∅ → dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) = (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
49	47, 48	ax-mp 5	. . . . . . . . . . 11 ⊢ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) = (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)
50	49	uneq2i 4097	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) = (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
51		undif2 4407	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
52	45, 50, 51	3eqtri 2762	. . . . . . . . 9 ⊢ dom 𝑍 = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
53		dmeq 5847	. . . . . . . . 9 ⊢ (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏)
54	52, 53	eqtr3id 2784	. . . . . . . 8 ⊢ (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏)
55	41, 54	nsyl 140	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏)
56		df-ne 2931	. . . . . . . 8 ⊢ (𝑍 ≠ 𝑏 ↔ ¬ 𝑍 = 𝑏)
57		notnotr 130	. . . . . . . . . . . . . . 15 ⊢ (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → dom (𝑏 ↾ dom 𝑆) = dom 𝑆)
58		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆)
59	58	fvresd 6849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
60	42	reseq1i 5929	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) ↾ dom 𝑆)
61		resundir 5948	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆))
62		df-res 5632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ∩ (dom 𝑆 × V))
63		disjdifr 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅
64		xpdisj1 6114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ∩ (dom 𝑆 × V)) = ∅)
65	63, 64	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ∩ (dom 𝑆 × V)) = ∅
66	62, 65	eqtri 2758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆) = ∅
67	66	uneq2i 4097	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
68		un0 4324	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆)
69	67, 68	eqtri 2758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆)
70	60, 61, 69	3eqtri 2762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆)
71		simplll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
72	6	nosupno 27655	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑆 ∈ No )
74	73	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑆 ∈ No )
75		nofun 27601	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ No → Fun 𝑆)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun 𝑆)
77		funrel 6504	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun 𝑆 → Rel 𝑆)
78		resdm 5980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
79	76, 77, 78	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆)
80	70, 79	eqtrid 2782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
81	80	fveq1d 6831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
82	59, 81	eqtr3d 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
83		simp-4l 783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ⊆ No )
84		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ∈ V)
85		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ∈ V)
86	85	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐵 ∈ V)
87	6, 42	noetasuplem1 27685	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 ∈ No )
88	83, 84, 86, 87	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 ∈ No )
89	88	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 ∈ No )
90	11	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑏 ∈ No )
91	90	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑏 ∈ No )
92		simplr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 ≠ 𝑏)
93		nosepne 27632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
94	89, 91, 92, 93	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
95	82, 94	eqnetrrd 2998	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
96	58	fvresd 6849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
97	95, 96	neeqtrrd 3004	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
98		fveq2 6829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
99		fveq2 6829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (𝑆‘𝑞) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
100	98, 99	neeq12d 2991	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
101		df-ne 2931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
102		necom 2983	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
103	100, 101, 102	3bitr3g 313	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
104	103	rspcev 3562	. . . . . . . . . . . . . . . . . 18 ⊢ ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∧ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
105	58, 97, 104	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
106		rexeq 3289	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
107	105, 106	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
108		rexnal 3087	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
109	107, 108	imbitrdi 251	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
110	57, 109	syl5 34	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
111	110	orrd 864	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
112		nofun 27601	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ No → Fun 𝑏)
113		funres 6529	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑏 → Fun (𝑏 ↾ dom 𝑆))
114	91, 112, 113	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆))
115		eqfunfv 6977	. . . . . . . . . . . . . . . 16 ⊢ ((Fun (𝑏 ↾ dom 𝑆) ∧ Fun 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
116	114, 76, 115	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
117		ianor 984	. . . . . . . . . . . . . . . 16 ⊢ (¬ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
118	117	con1bii 356	. . . . . . . . . . . . . . 15 ⊢ (¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
119	116, 118	bitr4di 289	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ ¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
120	119	con2bid 354	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ ¬ (𝑏 ↾ dom 𝑆) = 𝑆))
121	111, 120	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) = 𝑆)
122	121	pm2.21d 121	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 → 𝑍 <s 𝑏))
123	80	breq1d 5084	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆)))
124		nodmon 27602	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ No → dom 𝑆 ∈ On)
125	74, 124	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On)
126		ltsres 27614	. . . . . . . . . . . . 13 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑆 ∈ On) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
127	89, 91, 125, 126	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
128	123, 127	sylbird 260	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
129		simplrr 778	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
130	129	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
131		noreson 27612	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ No ∧ dom 𝑆 ∈ On) → (𝑏 ↾ dom 𝑆) ∈ No )
132	91, 125, 131	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑏 ↾ dom 𝑆) ∈ No )
133		ltsso 27628	. . . . . . . . . . . . . . 15 ⊢ <s Or No
134		sotric 5558	. . . . . . . . . . . . . . 15 ⊢ (( <s Or No ∧ ((𝑏 ↾ dom 𝑆) ∈ No ∧ 𝑆 ∈ No )) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
135	133, 134	mpan 691	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ↾ dom 𝑆) ∈ No ∧ 𝑆 ∈ No ) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
136	132, 74, 135	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
137	136	con2bid 354	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)) ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
138	130, 137	mpbird 257	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)))
139	122, 128, 138	mpjaod 861	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 <s 𝑏)
140	88	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 ∈ No )
141	90	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ∈ No )
142		simplr 769	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 ≠ 𝑏)
143	42	fveq1i 6830	. . . . . . . . . . . . 13 ⊢ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
144		simp-4l 783	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
145	144, 72, 75	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → Fun 𝑆)
146		funfn 6517	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑆 ↔ 𝑆 Fn dom 𝑆)
147	145, 146	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑆 Fn dom 𝑆)
148	46	fconst 6715	. . . . . . . . . . . . . . . 16 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1_o}
149		ffn 6657	. . . . . . . . . . . . . . . 16 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1_o} → ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
150	148, 149	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)
151	150	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
152		disjdif 4402	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅
153	152	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅)
154		necom 2983	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑍‘𝑝) ≠ (𝑏‘𝑝) ↔ (𝑏‘𝑝) ≠ (𝑍‘𝑝))
155	154	rabbii 3392	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
156	155	inteqi 4883	. . . . . . . . . . . . . . . . 17 ⊢ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
157	142	necomd 2985	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ≠ 𝑍)
158		nosepssdm 27638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ No ∧ 𝑍 ∈ No ∧ 𝑏 ≠ 𝑍) → ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏)
159	141, 140, 157, 158	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏)
160	156, 159	eqsstrid 3955	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏)
161	141, 16	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ( bday ‘𝑏) = dom 𝑏)
162		simplrl 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ⊆ No )
163	162	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐵 ⊆ No )
164	163	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝐵 ⊆ No )
165		simplrl 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑏 ∈ 𝐵)
166	165	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ∈ 𝐵)
167	164, 166, 22	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
168	161, 167	eqeltrrd 2836	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ∈ ( bday “ 𝐵))
169	168, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
170	141, 27, 35	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)))
171	169, 170	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ∈ suc ∪ ( bday “ 𝐵))
172		nosepon 27617	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
173	140, 141, 142, 172	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
174		eloni 6322	. . . . . . . . . . . . . . . . 17 ⊢ (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
175		ordsuc 7754	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ∪ ( bday “ 𝐵) ↔ Ord suc ∪ ( bday “ 𝐵))
176	33, 175	mpbi 230	. . . . . . . . . . . . . . . . . 18 ⊢ Ord suc ∪ ( bday “ 𝐵)
177		ordtr2 6357	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐵)) → ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵)))
178	176, 177	mpan2 692	. . . . . . . . . . . . . . . . 17 ⊢ (Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵)))
179	173, 174, 178	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵)))
180	160, 171, 179	mp2and 700	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵))
181		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
182	144, 72, 124	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑆 ∈ On)
183		ontri1 6346	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑆 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On) → (dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆))
184	182, 173, 183	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆))
185	181, 184	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ¬ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆)
186	180, 185	eldifd 3896	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
187		fvun2 6921	. . . . . . . . . . . . . 14 ⊢ ((𝑆 Fn dom 𝑆 ∧ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∧ ((dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅ ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))) → ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
188	147, 151, 153, 186, 187	syl112anc 1377	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
189	143, 188	eqtrid 2782	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
190	46	fvconst2 7148	. . . . . . . . . . . . 13 ⊢ (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o)
191	186, 190	syl 17	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o)
192	189, 191	eqtrd 2770	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o)
193		nosep1o 27633	. . . . . . . . . . 11 ⊢ (((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) ∧ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o) → 𝑍 <s 𝑏)
194	140, 141, 142, 192, 193	syl31anc 1376	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 <s 𝑏)
195		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 ≠ 𝑏)
196	88, 90, 195, 172	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
197	196, 174	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
198		nodmord 27605	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ No → Ord dom 𝑆)
199	71, 72, 198	3syl 18	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord dom 𝑆)
200		ordtri2or 6412	. . . . . . . . . . 11 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord dom 𝑆) → (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
201	197, 199, 200	syl2anc 585	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
202	139, 194, 201	mpjaodan 961	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 <s 𝑏)
203	202	ex 412	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (𝑍 ≠ 𝑏 → 𝑍 <s 𝑏))
204	56, 203	biimtrrid 243	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (¬ 𝑍 = 𝑏 → 𝑍 <s 𝑏))
205	55, 204	mpd 15	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑍 <s 𝑏)
206	205	expr 456	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (¬ (𝑏 ↾ dom 𝑆) <s 𝑆 → 𝑍 <s 𝑏))
207	8, 206	sylbid 240	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 → 𝑍 <s 𝑏))
208	207	ralimdva 3147	. . 3 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
209	1, 208	biimtrid 242	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
210	209	3impia 1118	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 {cab 2713 ≠ wne 2930 ∀wral 3049 ∃wrex 3059 {crab 3387 Vcvv 3427 ∖ cdif 3882 ∪ cun 3883 ∩ cin 3884 ⊆ wss 3885 ∅c0 4263 ifcif 4456 {csn 4557 ⟨cop 4563 ∪ cuni 4840 ∩ cint 4879 class class class wbr 5074 ↦ cmpt 5155 Or wor 5527 × cxp 5618 dom cdm 5620 ran crn 5621 ↾ cres 5622 “ cima 5623 Rel wrel 5625 Ord word 6311 Oncon0 6312 suc csuc 6314 ℩cio 6441 Fun wfun 6481 Fn wfn 6482 ⟶wf 6483 –onto→wfo 6485 ‘cfv 6487 ℩crio 7312 1_oc1o 8387 2_oc2o 8388 No csur 27591 <s clts 27592 bday cbday 27593

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2184 ax-ext 2707 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7678

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2931 df-ral 3050 df-rex 3060 df-rmo 3340 df-reu 3341 df-rab 3388 df-v 3429 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4841 df-int 4880 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-ord 6315 df-on 6316 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-riota 7313 df-1o 8394 df-2o 8395 df-no 27594 df-lts 27595 df-bday 27596

This theorem is referenced by: noetalem1 27693

W3C validator