Theorem noetasuplem4 27708

Description: Lemma for noeta 27715. 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 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
noetasuplem.2	⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))

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 3265	. . 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 3934	. . . . . 6 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
6		noetasuplem.1	. . . . . . 7 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
7	6	nosupbnd2 27688	. . . . . 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 3929	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ No ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
11	4, 9, 10	syl2an 597	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 ∈ No )
12		nodmord 27625	. . . . . . . . . 10 ⊢ (𝑏 ∈ No → Ord dom 𝑏)
13		ordirr 6336	. . . . . . . . . 10 ⊢ (Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏)
14	11, 12, 13	3syl 18	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏)
15		ssun2 4132	. . . . . . . . . . 11 ⊢ suc ∪ ( bday “ 𝐵) ⊆ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
16		bdayval 27620	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ No → ( bday ‘𝑏) = dom 𝑏)
17	11, 16	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday ‘𝑏) = dom 𝑏)
18		bdayfo 27649	. . . . . . . . . . . . . . . . 17 ⊢ bday : No –onto→On
19		fofn 6749	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → bday Fn No )
20	18, 19	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ bday Fn No
21		fnfvima 7181	. . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday “ 𝐵))
25		elssuni 4895	. . . . . . . . . . . . 13 ⊢ (dom 𝑏 ∈ ( bday “ 𝐵) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
26	24, 25	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ⊆ ∪ ( bday “ 𝐵))
27		nodmon 27622	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ No → dom 𝑏 ∈ On)
28		imassrn 6031	. . . . . . . . . . . . . . . 16 ⊢ ( bday “ 𝐵) ⊆ ran bday
29		forn 6750	. . . . . . . . . . . . . . . . 17 ⊢ ( bday : No –onto→On → ran bday = On)
30	18, 29	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ran bday = On
31	28, 30	sseqtri 3983	. . . . . . . . . . . . . . 15 ⊢ ( bday “ 𝐵) ⊆ On
32		ssorduni 7726	. . . . . . . . . . . . . . 15 ⊢ (( bday “ 𝐵) ⊆ On → Ord ∪ ( bday “ 𝐵))
33	31, 32	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Ord ∪ ( bday “ 𝐵)
34		ordsssuc 6409	. . . . . . . . . . . . . 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 3932	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)))
39		eleq2 2826	. . . . . . . . . 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 𝑆) × {1o}))
43	42	dmeqi 5854	. . . . . . . . . . 11 ⊢ dom 𝑍 = dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))
44		dmun 5860	. . . . . . . . . . 11 ⊢ dom (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))
45	43, 44	eqtri 2760	. . . . . . . . . 10 ⊢ dom 𝑍 = (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))
46		1oex 8409	. . . . . . . . . . . . 13 ⊢ 1o ∈ V
47	46	snnz 4734	. . . . . . . . . . . 12 ⊢ {1o} ≠ ∅
48		dmxp 5879	. . . . . . . . . . . 12 ⊢ ({1o} ≠ ∅ → dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) = (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
49	47, 48	ax-mp 5	. . . . . . . . . . 11 ⊢ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) = (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)
50	49	uneq2i 4118	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ dom ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
51		undif2 4430	. . . . . . . . . 10 ⊢ (dom 𝑆 ∪ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
52	45, 50, 51	3eqtri 2764	. . . . . . . . 9 ⊢ dom 𝑍 = (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵))
53		dmeq 5853	. . . . . . . . 9 ⊢ (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏)
54	52, 53	eqtr3id 2786	. . . . . . . 8 ⊢ (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ∪ ( bday “ 𝐵)) = dom 𝑏)
55	41, 54	nsyl 140	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏)
56		df-ne 2934	. . . . . . . 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 6855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
60	42	reseq1i 5935	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆)
61		resundir 5954	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆))
62		df-res 5637	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V))
63		disjdifr 4426	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅
64		xpdisj1 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) = ∅)
65	63, 64	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) = ∅
66	62, 65	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅
67	66	uneq2i 4118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
68		un0 4347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆)
69	67, 68	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ↾ dom 𝑆) ∪ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆)
70	60, 61, 69	3eqtri 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆)
71		simplll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
72	6	nosupno 27675	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 27621	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ No → Fun 𝑆)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun 𝑆)
77		funrel 6510	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun 𝑆 → Rel 𝑆)
78		resdm 5986	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
79	76, 77, 78	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆)
80	70, 79	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
81	80	fveq1d 6837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
82	59, 81	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . 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 27705	. . . . . . . . . . . . . . . . . . . . . . 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 27652	. . . . . . . . . . . . . . . . . . . . 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 3001	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
96	58	fvresd 6855	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (𝑏‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
97	95, 96	neeqtrrd 3007	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
98		fveq2 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
99		fveq2 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (𝑆‘𝑞) = (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
100	98, 99	neeq12d 2994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
101		df-ne 2934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆‘𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞))
102		necom 2986	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
103	100, 101, 102	3bitr3g 313	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆‘𝑞) ↔ (𝑆‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})))
104	103	rspcev 3577	. . . . . . . . . . . . . . . . . 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 3293	. . . . . . . . . . . . . . . . 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 3089	. . . . . . . . . . . . . . . 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 27621	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ No → Fun 𝑏)
113		funres 6535	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑏 → Fun (𝑏 ↾ dom 𝑆))
114	91, 112, 113	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆))
115		eqfunfv 6983	. . . . . . . . . . . . . . . 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 5109	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆)))
124		nodmon 27622	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ No → dom 𝑆 ∈ On)
125	74, 124	syl 17	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On)
126		ltsres 27634	. . . . . . . . . . . . 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 27632	. . . . . . . . . . . . . . 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 27648	. . . . . . . . . . . . . . 15 ⊢ <s Or No
134		sotric 5563	. . . . . . . . . . . . . . 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 6836	. . . . . . . . . . . . 13 ⊢ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))‘∩ {𝑝 ∈ 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 6523	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑆 ↔ 𝑆 Fn dom 𝑆)
147	145, 146	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑆 Fn dom 𝑆)
148	46	fconst 6721	. . . . . . . . . . . . . . . 16 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1o}
149		ffn 6663	. . . . . . . . . . . . . . . 16 ⊢ (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}):(suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)⟶{1o} → ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
150	148, 149	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)
151	150	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
152		disjdif 4425	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅
153	152	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅)
154		necom 2986	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑍‘𝑝) ≠ (𝑏‘𝑝) ↔ (𝑏‘𝑝) ≠ (𝑍‘𝑝))
155	154	rabbii 3405	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
156	155	inteqi 4907	. . . . . . . . . . . . . . . . 17 ⊢ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} = ∩ {𝑝 ∈ On ∣ (𝑏‘𝑝) ≠ (𝑍‘𝑝)}
157	142	necomd 2988	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → 𝑏 ≠ 𝑍)
158		nosepssdm 27658	. . . . . . . . . . . . . . . . . 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 3973	. . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . . . 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 27637	. . . . . . . . . . . . . . . . . 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 6328	. . . . . . . . . . . . . . . . 17 ⊢ (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ On → Ord ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)})
175		ordsuc 7758	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ∪ ( bday “ 𝐵) ↔ Ord suc ∪ ( bday “ 𝐵))
176	33, 175	mpbi 230	. . . . . . . . . . . . . . . . . 18 ⊢ Ord suc ∪ ( bday “ 𝐵)
177		ordtr2 6363	. . . . . . . . . . . . . . . . . 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 6352	. . . . . . . . . . . . . . . . 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 3913	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))
187		fvun2 6927	. . . . . . . . . . . . . 14 ⊢ ((𝑆 Fn dom 𝑆 ∧ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) ∧ ((dom 𝑆 ∩ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆)) = ∅ ∧ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆))) → ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
188	147, 151, 153, 186, 187	syl112anc 1377	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → ((𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
189	143, 188	eqtrid 2784	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}))
190	46	fvconst2 7152	. . . . . . . . . . . . 13 ⊢ (∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)} ∈ (suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o)
191	186, 190	syl 17	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o})‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o)
192	189, 191	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) ∧ dom 𝑆 ⊆ ∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) → (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o)
193		nosep1o 27653	. . . . . . . . . . 11 ⊢ (((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 ≠ 𝑏) ∧ (𝑍‘∩ {𝑝 ∈ On ∣ (𝑍‘𝑝) ≠ (𝑏‘𝑝)}) = 1o) → 𝑍 <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 27625	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ No → Ord dom 𝑆)
199	71, 72, 198	3syl 18	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ (𝑏 ∈ 𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍 ≠ 𝑏) → Ord dom 𝑆)
200		ordtri2or 6418	. . . . . . . . . . 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 3149	. . 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 𝑏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2715   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3400  Vcvv 3441   ∖ cdif 3899   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4286  ifcif 4480  {csn 4581  ⟨cop 4587  ∪ cuni 4864  ∩ cint 4903   class class class wbr 5099   ↦ cmpt 5180   Or wor 5532   × cxp 5623  dom cdm 5625  ran crn 5626   ↾ cres 5627   “ cima 5628  Rel wrel 5630  Ord word 6317  Oncon0 6318  suc csuc 6320  ℩cio 6447  Fun wfun 6487   Fn wfn 6488  ⟶wf 6489  –onto→wfo 6491  ‘cfv 6493  ℩crio 7316  1_oc1o 8392  2_oc2o 8393   No csur 27611   <s clts 27612   bday cbday 27613

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 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4865  df-int 4904  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-1o 8399  df-2o 8400  df-no 27614  df-lts 27615  df-bday 27616

This theorem is referenced by:  noetalem1  27713