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 27683

Description: Lemma for noeta 27690. 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 774	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ⊆ No )
3		simpllr 775	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ V)
4		simprl 770	. . . . . . 7 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → 𝐵 ⊆ No )
5	4	sselda 3943	. . . . . 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 27663	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑏 ∈ No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
8	2, 3, 5, 7	syl3anc 1373	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
9		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) → 𝑏 ∈ 𝐵)
10		ssel2 3938	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
11	4, 9, 10	syl2an 596	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 ∈ No )
12		nodmord 27600	. . . . . . . . . 10 ⊢ (𝑏 ∈ No → Ord dom 𝑏)
13		ordirr 6339	. . . . . . . . . 10 ⊢ (Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏)
14	11, 12, 13	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏)
15		ssun2 4138	. . . . . . . . . . 11 ⊢ suc ∪ ( bday “ 𝐵) ⊆ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
16		bdayval 27595	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ No → ( bday ‘𝑏) = dom 𝑏)
17	11, 16	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday ‘𝑏) = dom 𝑏)
18		bdayfo 27624	. . . . . . . . . . . . . . . . 17 ⊢ bday : No –onto→On
19		fofn 6757	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → bday Fn No )
20	18, 19	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ bday Fn No
21		fnfvima 7190	. . . . . . . . . . . . . . . 16 ⊢ (( bday Fn No ∧ 𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
22	20, 21	mp3an1 1450	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
23	4, 9, 22	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
24	17, 23	eqeltrrd 2829	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday “ 𝐵))
25		elssuni 4897	. . . . . . . . . . . . 13 ⊢ (dom 𝑏 ∈ ( bday “ 𝐵) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
27		nodmon 27597	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ No → dom 𝑏 ∈ On)
28		imassrn 6032	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐵) ⊆ ran bday
29		forn 6758	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
30	18, 29	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
31	28, 30	sseqtri 3992	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐵) ⊆ On
32		ssorduni 7736	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐵) ⊆ On → Ord ∪ ( bday “ 𝐵))
33	31, 32	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐵)
34		ordsssuc 6412	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑏 ∈ On ∧ Ord ∪ ( bday “ 𝐵)) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)))
35	33, 34	mpan2 691	. . . . . . . . . . . . 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 3941	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)))
39		eleq2 2817	. . . . . . . . . 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 5859	. . . . . . . . . . 11 ⊢ dom 𝑍 = dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
44		dmun 5865	. . . . . . . . . . 11 ⊢ dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
45	43, 44	eqtri 2752	. . . . . . . . . 10 ⊢ dom 𝑍 = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
46		1oex 8422	. . . . . . . . . . . . 13 ⊢ 1_o ∈ V
47	46	snnz 4736	. . . . . . . . . . . 12 ⊢ {1_o} ≠ ∅
48		dmxp 5883	. . . . . . . . . . . 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 4124	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) = (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
51		undif2 4436	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
52	45, 50, 51	3eqtri 2756	. . . . . . . . 9 ⊢ dom 𝑍 = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
53		dmeq 5858	. . . . . . . . 9 ⊢ (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏)
54	52, 53	eqtr3id 2778	. . . . . . . 8 ⊢ (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏)
55	41, 54	nsyl 140	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏)
56		df-ne 2926	. . . . . . . 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 6861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
60	42	reseq1i 5936	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) ↾ dom 𝑆)
61		resundir 5955	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆))
62		df-res 5643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ∩ (dom 𝑆 × V))
63		disjdifr 4432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅
64		xpdisj1 6123	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆) = ∅
67	66	uneq2i 4124	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
68		un0 4353	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆)
69	67, 68	eqtri 2752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆)
70	60, 61, 69	3eqtri 2756	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆)
71		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
72	6	nosupno 27650	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 27596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ No → Fun 𝑆)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun 𝑆)
77		funrel 6518	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun 𝑆 → Rel 𝑆)
78		resdm 5987	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
79	76, 77, 78	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆)
80	70, 79	eqtrid 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
81	80	fveq1d 6843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
82	59, 81	eqtr3d 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
83		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ⊆ No )
84		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ∈ V)
85		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ∈ V)
86	85	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐵 ∈ V)
87	6, 42	noetasuplem1 27680	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 ∈ No )
88	83, 84, 86, 87	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 ≠ 𝑏)
93		nosepne 27627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
94	89, 91, 92, 93	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
95	82, 94	eqnetrrd 2993	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
96	58	fvresd 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
97	95, 96	neeqtrrd 2999	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
98		fveq2 6841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
99		fveq2 6841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (𝑆‘𝑞) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
100	98, 99	neeq12d 2986	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
101		df-ne 2926	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
102		necom 2978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
103	100, 101, 102	3bitr3g 313	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
104	103	rspcev 3585	. . . . . . . . . . . . . . . . . 18 ⊢ ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∧ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
105	58, 97, 104	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
106		rexeq 3292	. . . . . . . . . . . . . . . . 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 3082	. . . . . . . . . . . . . . . 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 863	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
112		nofun 27596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ No → Fun 𝑏)
113		funres 6543	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑏 → Fun (𝑏 ↾ dom 𝑆))
114	91, 112, 113	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆))
115		eqfunfv 6991	. . . . . . . . . . . . . . . 16 ⊢ ((Fun (𝑏 ↾ dom 𝑆) ∧ Fun 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
116	114, 76, 115	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
117		ianor 983	. . . . . . . . . . . . . . . 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 5112	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆)))
124		nodmon 27597	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ No → dom 𝑆 ∈ On)
125	74, 124	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On)
126		sltres 27609	. . . . . . . . . . . . 13 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑆 ∈ On) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
127	89, 91, 125, 126	syl3anc 1373	. . . . . . . . . . . 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 777	. . . . . . . . . . . . 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 27607	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ No ∧ dom 𝑆 ∈ On) → (𝑏 ↾ dom 𝑆) ∈ No )
132	91, 125, 131	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑏 ↾ dom 𝑆) ∈ No )
133		sltso 27623	. . . . . . . . . . . . . . 15 ⊢ <s Or No
134		sotric 5569	. . . . . . . . . . . . . . 15 ⊢ (( <s Or No ∧ ((𝑏 ↾ dom 𝑆) ∈ No ∧ 𝑆 ∈ No )) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
135	133, 134	mpan 690	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ↾ dom 𝑆) ∈ No ∧ 𝑆 ∈ No ) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
136	132, 74, 135	syl2anc 584	. . . . . . . . . . . . 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 860	. . . . . . . . . 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 768	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 ≠ 𝑏)
143	42	fveq1i 6842	. . . . . . . . . . . . 13 ⊢ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
144		simp-4l 782	. . . . . . . . . . . . . . . 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 6531	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑆 ↔ 𝑆 Fn dom 𝑆)
147	145, 146	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑆 Fn dom 𝑆)
148	46	fconst 6729	. . . . . . . . . . . . . . . 16 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1_o}
149		ffn 6671	. . . . . . . . . . . . . . . 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 4431	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅
153	152	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅)
154		necom 2978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑍‘𝑝) ≠ (𝑏‘𝑝) ↔ (𝑏‘𝑝) ≠ (𝑍‘𝑝))
155	154	rabbii 3408	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
156	155	inteqi 4910	. . . . . . . . . . . . . . . . 17 ⊢ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
157	142	necomd 2980	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ≠ 𝑍)
158		nosepssdm 27633	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ No ∧ 𝑍 ∈ No ∧ 𝑏 ≠ 𝑍) → ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏)
159	141, 140, 157, 158	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏)
160	156, 159	eqsstrid 3982	. . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
168	161, 167	eqeltrrd 2829	. . . . . . . . . . . . . . . . . 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 27612	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
173	140, 141, 142, 172	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
174		eloni 6331	. . . . . . . . . . . . . . . . 17 ⊢ (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
175		ordsuc 7769	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ∪ ( bday “ 𝐵) ↔ Ord suc ∪ ( bday “ 𝐵))
176	33, 175	mpbi 230	. . . . . . . . . . . . . . . . . 18 ⊢ Ord suc ∪ ( bday “ 𝐵)
177		ordtr2 6366	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐵)) → ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵)))
178	176, 177	mpan2 691	. . . . . . . . . . . . . . . . 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 699	. . . . . . . . . . . . . . 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 6355	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑆 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On) → (dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆))
184	182, 173, 183	syl2anc 584	. . . . . . . . . . . . . . . 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 3922	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
187		fvun2 6936	. . . . . . . . . . . . . 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 1376	. . . . . . . . . . . . 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 2776	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
190	46	fvconst2 7161	. . . . . . . . . . . . 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 2764	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o)
193		nosep1o 27628	. . . . . . . . . . 11 ⊢ (((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) ∧ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o) → 𝑍 <s 𝑏)
194	140, 141, 142, 192, 193	syl31anc 1375	. . . . . . . . . 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 1373	. . . . . . . . . . . 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 27600	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ No → Ord dom 𝑆)
199	71, 72, 198	3syl 18	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord dom 𝑆)
200		ordtri2or 6421	. . . . . . . . . . 11 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord dom 𝑆) → (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
201	197, 199, 200	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
202	139, 194, 201	mpjaodan 960	. . . . . . . . 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 3145	. . 3 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
209	1, 208	biimtrid 242	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
210	209	3impia 1117	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 {cab 2707 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3402 Vcvv 3444 ∖ cdif 3908 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 ifcif 4484 {csn 4585 ⟨cop 4591 ∪ cuni 4867 ∩ cint 4906 class class class wbr 5102 ↦ cmpt 5183 Or wor 5538 × cxp 5629 dom cdm 5631 ran crn 5632 ↾ cres 5633 “ cima 5634 Rel wrel 5636 Ord word 6320 Oncon0 6321 suc csuc 6323 ℩cio 6451 Fun wfun 6494 Fn wfn 6495 ⟶wf 6496 –onto→wfo 6498 ‘cfv 6500 ℩crio 7326 1_oc1o 8405 2_oc2o 8406 No csur 27586 <s cslt 27587 bday cbday 27588

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7692

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-ord 6324 df-on 6325 df-suc 6327 df-iota 6453 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7327 df-1o 8412 df-2o 8413 df-no 27589 df-slt 27590 df-bday 27591

This theorem is referenced by: noetalem1 27688

W3C validator