noetasuplem4 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > noetasuplem4		Structured version Visualization version GIF version

Theorem noetasuplem4 33528

Description: Lemma for noeta 33535. 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 3272	. . 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 3894	. . . . . 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 33508	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑏 ∈ No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
8	2, 3, 5, 7	syl3anc 1368	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
9		simpl 486	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) → 𝑏 ∈ 𝐵)
10		ssel2 3889	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
11	4, 9, 10	syl2an 598	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 ∈ No )
12		nodmord 33445	. . . . . . . . . 10 ⊢ (𝑏 ∈ No → Ord dom 𝑏)
13		ordirr 6191	. . . . . . . . . 10 ⊢ (Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏)
14	11, 12, 13	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏)
15		ssun2 4080	. . . . . . . . . . 11 ⊢ suc ∪ ( bday “ 𝐵) ⊆ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
16		bdayval 33440	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ No → ( bday ‘𝑏) = dom 𝑏)
17	11, 16	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday ‘𝑏) = dom 𝑏)
18		bdayfo 33469	. . . . . . . . . . . . . . . . 17 ⊢ bday : No –onto→On
19		fofn 6582	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → bday Fn No )
20	18, 19	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ bday Fn No
21		fnfvima 6992	. . . . . . . . . . . . . . . 16 ⊢ (( bday Fn No ∧ 𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
22	20, 21	mp3an1 1445	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
23	4, 9, 22	syl2an 598	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
24	17, 23	eqeltrrd 2853	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday “ 𝐵))
25		elssuni 4833	. . . . . . . . . . . . 13 ⊢ (dom 𝑏 ∈ ( bday “ 𝐵) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
27		nodmon 33442	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ No → dom 𝑏 ∈ On)
28		imassrn 5916	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐵) ⊆ ran bday
29		forn 6583	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
30	18, 29	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
31	28, 30	sseqtri 3930	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐵) ⊆ On
32		ssorduni 7504	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐵) ⊆ On → Ord ∪ ( bday “ 𝐵))
33	31, 32	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐵)
34		ordsssuc 6259	. . . . . . . . . . . . . 14 ⊢ ((dom 𝑏 ∈ On ∧ Ord ∪ ( bday “ 𝐵)) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)))
35	33, 34	mpan2 690	. . . . . . . . . . . . 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 235	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ suc ∪ ( bday “ 𝐵))
38	15, 37	sseldi 3892	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)))
39		eleq2 2840	. . . . . . . . . 10 ⊢ ((dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏 → (dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) ↔ dom 𝑏 ∈ dom 𝑏))
40	38, 39	syl5ibcom 248	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ((dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏 → dom 𝑏 ∈ dom 𝑏))
41	14, 40	mtod 201	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏)
42		noetasuplem.2	. . . . . . . . . . . 12 ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
43	42	dmeqi 5749	. . . . . . . . . . 11 ⊢ dom 𝑍 = dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
44		dmun 5755	. . . . . . . . . . 11 ⊢ dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
45	43, 44	eqtri 2781	. . . . . . . . . 10 ⊢ dom 𝑍 = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))
46		1oex 8125	. . . . . . . . . . . . 13 ⊢ 1_o ∈ V
47	46	snnz 4672	. . . . . . . . . . . 12 ⊢ {1_o} ≠ ∅
48		dmxp 5774	. . . . . . . . . . . 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 4067	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) = (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
51		undif2 4376	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
52	45, 50, 51	3eqtri 2785	. . . . . . . . 9 ⊢ dom 𝑍 = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
53		dmeq 5748	. . . . . . . . 9 ⊢ (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏)
54	52, 53	syl5eqr 2807	. . . . . . . 8 ⊢ (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏)
55	41, 54	nsyl 142	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏)
56		df-ne 2952	. . . . . . . 8 ⊢ (𝑍 ≠ 𝑏 ↔ ¬ 𝑍 = 𝑏)
57		notnotr 132	. . . . . . . . . . . . . . 15 ⊢ (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → dom (𝑏 ↾ dom 𝑆) = dom 𝑆)
58		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆)
59	58	fvresd 6682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
60	42	reseq1i 5823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) ↾ dom 𝑆)
61		resundir 5842	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆))
62		df-res 5539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ∩ (dom 𝑆 × V))
63		incom 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
64		disjdif 4371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅
65	63, 64	eqtri 2781	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅
66		xpdisj1 5994	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ∩ (dom 𝑆 × V)) = ∅)
67	65, 66	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ∩ (dom 𝑆 × V)) = ∅
68	62, 67	eqtri 2781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆) = ∅
69	68	uneq2i 4067	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
70		un0 4289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆)
71	69, 70	eqtri 2781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆)
72	60, 61, 71	3eqtri 2785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆)
73		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
74	6	nosupno 33495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑆 ∈ No )
76	75	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑆 ∈ No )
77		nofun 33441	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ No → Fun 𝑆)
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun 𝑆)
79		funrel 6356	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun 𝑆 → Rel 𝑆)
80		resdm 5872	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
81	78, 79, 80	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆)
82	72, 81	syl5eq 2805	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
83	82	fveq1d 6664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
84	59, 83	eqtr3d 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
85		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ⊆ No )
86		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐴 ∈ V)
87		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ∈ V)
88	87	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐵 ∈ V)
89	6, 42	noetasuplem1 33525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 ∈ No )
90	85, 86, 88, 89	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 ∈ No )
91	90	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 ∈ No )
92	11	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑏 ∈ No )
93	92	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑏 ∈ No )
94		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 ≠ 𝑏)
95		nosepne 33472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
96	91, 93, 94, 95	syl3anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
97	84, 96	eqnetrrd 3019	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
98	58	fvresd 6682	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
99	97, 98	neeqtrrd 3025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
100		fveq2 6662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
101		fveq2 6662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (𝑆‘𝑞) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
102	100, 101	neeq12d 3012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
103		df-ne 2952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
104		necom 3004	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
105	102, 103, 104	3bitr3g 316	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
106	105	rspcev 3543	. . . . . . . . . . . . . . . . . 18 ⊢ ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∧ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
107	58, 99, 106	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
108		rexeq 3324	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
109	107, 108	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
110		rexnal 3165	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
111	109, 110	syl6ib 254	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
112	57, 111	syl5 34	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
113	112	orrd 860	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
114		nofun 33441	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ No → Fun 𝑏)
115		funres 6381	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑏 → Fun (𝑏 ↾ dom 𝑆))
116	93, 114, 115	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆))
117		eqfunfv 6802	. . . . . . . . . . . . . . . 16 ⊢ ((Fun (𝑏 ↾ dom 𝑆) ∧ Fun 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
118	116, 78, 117	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
119		ianor 979	. . . . . . . . . . . . . . . 16 ⊢ (¬ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
120	119	con1bii 360	. . . . . . . . . . . . . . 15 ⊢ (¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)))
121	118, 120	bitr4di 292	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ ¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))))
122	121	con2bid 358	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞)) ↔ ¬ (𝑏 ↾ dom 𝑆) = 𝑆))
123	113, 122	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) = 𝑆)
124	123	pm2.21d 121	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 → 𝑍 <s 𝑏))
125	82	breq1d 5045	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆)))
126		nodmon 33442	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ No → dom 𝑆 ∈ On)
127	76, 126	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On)
128		sltres 33454	. . . . . . . . . . . . 13 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑆 ∈ On) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
129	91, 93, 127, 128	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
130	125, 129	sylbird 263	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
131		simplrr 777	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
132	131	adantr 484	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
133		noreson 33452	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ No ∧ dom 𝑆 ∈ On) → (𝑏 ↾ dom 𝑆) ∈ No )
134	93, 127, 133	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑏 ↾ dom 𝑆) ∈ No )
135		sltso 33468	. . . . . . . . . . . . . . 15 ⊢ <s Or No
136		sotric 5473	. . . . . . . . . . . . . . 15 ⊢ (( <s Or No ∧ ((𝑏 ↾ dom 𝑆) ∈ No ∧ 𝑆 ∈ No )) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
137	135, 136	mpan 689	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ↾ dom 𝑆) ∈ No ∧ 𝑆 ∈ No ) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
138	134, 76, 137	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆))))
139	138	con2bid 358	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)) ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
140	132, 139	mpbird 260	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 ↾ dom 𝑆)))
141	124, 130, 140	mpjaod 857	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → 𝑍 <s 𝑏)
142	90	adantr 484	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 ∈ No )
143	92	adantr 484	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ∈ No )
144		simplr 768	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 ≠ 𝑏)
145	42	fveq1i 6663	. . . . . . . . . . . . 13 ⊢ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
146		simp-4l 782	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
147	146, 74, 77	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → Fun 𝑆)
148		funfn 6369	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑆 ↔ 𝑆 Fn dom 𝑆)
149	147, 148	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑆 Fn dom 𝑆)
150	46	fconst 6554	. . . . . . . . . . . . . . . 16 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1_o}
151		ffn 6502	. . . . . . . . . . . . . . . 16 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1_o} → ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
152	150, 151	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)
153	152	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
154	64	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅)
155		necom 3004	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑍‘𝑝) ≠ (𝑏‘𝑝) ↔ (𝑏‘𝑝) ≠ (𝑍‘𝑝))
156	155	rabbii 3385	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
157	156	inteqi 4845	. . . . . . . . . . . . . . . . 17 ⊢ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
158	144	necomd 3006	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ≠ 𝑍)
159		nosepssdm 33478	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ No ∧ 𝑍 ∈ No ∧ 𝑏 ≠ 𝑍) → ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏)
160	143, 142, 158, 159	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)} ⊆ dom 𝑏)
161	157, 160	eqsstrid 3942	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏)
162	143, 16	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ( bday ‘𝑏) = dom 𝑏)
163		simplrl 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ⊆ No )
164	163	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝐵 ⊆ No )
165	164	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝐵 ⊆ No )
166		simplrl 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑏 ∈ 𝐵)
167	166	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ∈ 𝐵)
168	165, 167, 22	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ( bday ‘𝑏) ∈ ( bday “ 𝐵))
169	162, 168	eqeltrrd 2853	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ∈ ( bday “ 𝐵))
170	169, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
171	143, 27, 35	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑏 ⊆ ∪ ( bday “ 𝐵) ↔ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)))
172	170, 171	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑏 ∈ suc ∪ ( bday “ 𝐵))
173		nosepon 33457	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
174	142, 143, 144, 173	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
175		eloni 6183	. . . . . . . . . . . . . . . . 17 ⊢ (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
176		ordsuc 7533	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ∪ ( bday “ 𝐵) ↔ Ord suc ∪ ( bday “ 𝐵))
177	33, 176	mpbi 233	. . . . . . . . . . . . . . . . . 18 ⊢ Ord suc ∪ ( bday “ 𝐵)
178		ordtr2 6217	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord suc ∪ ( bday “ 𝐵)) → ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵)))
179	177, 178	mpan2 690	. . . . . . . . . . . . . . . . 17 ⊢ (Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵)))
180	174, 175, 179	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ∪ ( bday “ 𝐵)) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵)))
181	161, 172, 180	mp2and 698	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ suc ∪ ( bday “ 𝐵))
182		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
183	146, 74, 126	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → dom 𝑆 ∈ On)
184		ontri1 6207	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑆 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On) → (dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆))
185	183, 174, 184	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ↔ ¬ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆))
186	182, 185	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ¬ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆)
187	181, 186	eldifd 3871	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
188		fvun2 6748	. . . . . . . . . . . . . 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 ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
189	149, 153, 154, 187, 188	syl112anc 1371	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
190	145, 189	syl5eq 2805	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
191	46	fvconst2 6962	. . . . . . . . . . . . 13 ⊢ (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o)
192	187, 191	syl 17	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1_o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o)
193	190, 192	eqtrd 2793	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o)
194		nosep1o 33473	. . . . . . . . . . 11 ⊢ (((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) ∧ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1_o) → 𝑍 <s 𝑏)
195	142, 143, 144, 193, 194	syl31anc 1370	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑍 <s 𝑏)
196		simpr 488	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 ≠ 𝑏)
197	90, 92, 196, 173	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On)
198	197, 175	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
199		nodmord 33445	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ No → Ord dom 𝑆)
200	73, 74, 199	3syl 18	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord dom 𝑆)
201		ordtri2or 6268	. . . . . . . . . . 11 ⊢ ((Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∧ Ord dom 𝑆) → (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
202	198, 200, 201	syl2anc 587	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
203	141, 195, 202	mpjaodan 956	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → 𝑍 <s 𝑏)
204	203	ex 416	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (𝑍 ≠ 𝑏 → 𝑍 <s 𝑏))
205	56, 204	syl5bir 246	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (¬ 𝑍 = 𝑏 → 𝑍 <s 𝑏))
206	55, 205	mpd 15	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑍 <s 𝑏)
207	206	expr 460	. . . . 5 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (¬ (𝑏 ↾ dom 𝑆) <s 𝑆 → 𝑍 <s 𝑏))
208	8, 207	sylbid 243	. . . 4 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 → 𝑍 <s 𝑏))
209	208	ralimdva 3108	. . 3 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
210	1, 209	syl5bi 245	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏))
211	210	3impia 1114	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 {cab 2735 ≠ wne 2951 ∀wral 3070 ∃wrex 3071 {crab 3074 Vcvv 3409 ∖ cdif 3857 ∪ cun 3858 ∩ cin 3859 ⊆ wss 3860 ∅c0 4227 ifcif 4423 {csn 4525 ⟨cop 4531 ∪ cuni 4801 ∩ cint 4841 class class class wbr 5035 ↦ cmpt 5115 Or wor 5445 × cxp 5525 dom cdm 5527 ran crn 5528 ↾ cres 5529 “ cima 5530 Rel wrel 5532 Ord word 6172 Oncon0 6173 suc csuc 6175 ℩cio 6296 Fun wfun 6333 Fn wfn 6334 ⟶wf 6335 –onto→wfo 6337 ‘cfv 6339 ℩crio 7112 1_oc1o 8110 2_oc2o 8111 No csur 33432 <s cslt 33433 bday cbday 33434

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5159 ax-sep 5172 ax-nul 5179 ax-pr 5301 ax-un 7464

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-br 5036 df-opab 5098 df-mpt 5116 df-tr 5142 df-id 5433 df-eprel 5438 df-po 5446 df-so 5447 df-fr 5486 df-we 5488 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-ord 6176 df-on 6177 df-suc 6179 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-riota 7113 df-1o 8117 df-2o 8118 df-no 33435 df-slt 33436 df-bday 33437

This theorem is referenced by: noetalem1 33533

W3C validator