Theorem nofulllem5 31105

Description: Lemma for nofull (future) . Here, we introduce a new surreal number 𝑋. Eventually, we will show that either 𝑋 or a related surreal number has the required properties for the final theorem. We begin by calculating the domain of 𝑋. (Contributed by Scott Fenton, 1-May-2017.)

Hypotheses

Ref	Expression
nofulllem5.1	⊢ 𝑀 = ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}
nofulllem5.2	⊢ 𝑆 = {𝑓 ∣ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓)}
nofulllem5.3	⊢ 𝑋 = ∪ 𝑆

Assertion

Ref	Expression
nofulllem5	⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → dom 𝑋 = ∪ 𝑀)

Distinct variable groups:   𝑥,𝐿,𝑦,𝑓,𝑔,ℎ,𝑎   𝑥,𝑅,𝑦,ℎ,𝑓,𝑔,𝑎   𝑥,𝑊,𝑦,𝑓,𝑔,ℎ,𝑎   𝑥,𝑉,𝑦,𝑓,𝑔,ℎ,𝑎   𝑀,𝑎,𝑓,𝑔,ℎ

Allowed substitution hints:   𝑆(𝑥,𝑦,𝑓,𝑔,ℎ,𝑎)   𝑀(𝑥,𝑦)   𝑋(𝑥,𝑦,𝑓,𝑔,ℎ,𝑎)

Proof of Theorem nofulllem5

Dummy variables 𝑏 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nofulllem5.3	. . . 4 ⊢ 𝑋 = ∪ 𝑆
2	1	dmeqi 5247	. . 3 ⊢ dom 𝑋 = dom ∪ 𝑆
3		dmuni 5256	. . 3 ⊢ dom ∪ 𝑆 = ∪ 𝑏 ∈ 𝑆 dom 𝑏
4	2, 3	eqtri 2632	. 2 ⊢ dom 𝑋 = ∪ 𝑏 ∈ 𝑆 dom 𝑏
5		iunss 4497	. . . . 5 ⊢ (∪ 𝑏 ∈ 𝑆 dom 𝑏 ⊆ ∪ 𝑀 ↔ ∀𝑏 ∈ 𝑆 dom 𝑏 ⊆ ∪ 𝑀)
6		vex 3176	. . . . . . 7 ⊢ 𝑏 ∈ V
7		eqeq2 2621	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → ((𝑔 ↾ 𝑎) = 𝑓 ↔ (𝑔 ↾ 𝑎) = 𝑏))
8		eqeq2 2621	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → ((ℎ ↾ 𝑎) = 𝑓 ↔ (ℎ ↾ 𝑎) = 𝑏))
9	7, 8	anbi12d 743	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → (((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓) ↔ ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏)))
10	9	rexbidv 3034	. . . . . . . 8 ⊢ (𝑓 = 𝑏 → (∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓) ↔ ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏)))
11	10	2rexbidv 3039	. . . . . . 7 ⊢ (𝑓 = 𝑏 → (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓) ↔ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏)))
12		nofulllem5.2	. . . . . . 7 ⊢ 𝑆 = {𝑓 ∣ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓)}
13	6, 11, 12	elab2 3323	. . . . . 6 ⊢ (𝑏 ∈ 𝑆 ↔ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏))
14		inss1 3795	. . . . . . . . . . . 12 ⊢ (𝑎 ∩ dom 𝑔) ⊆ 𝑎
15		elssuni 4403	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑀 → 𝑎 ⊆ ∪ 𝑀)
16	14, 15	syl5ss 3579	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝑀 → (𝑎 ∩ dom 𝑔) ⊆ ∪ 𝑀)
17		dmres 5339	. . . . . . . . . . . . 13 ⊢ dom (𝑔 ↾ 𝑎) = (𝑎 ∩ dom 𝑔)
18		dmeq 5246	. . . . . . . . . . . . 13 ⊢ ((𝑔 ↾ 𝑎) = 𝑏 → dom (𝑔 ↾ 𝑎) = dom 𝑏)
19	17, 18	syl5eqr 2658	. . . . . . . . . . . 12 ⊢ ((𝑔 ↾ 𝑎) = 𝑏 → (𝑎 ∩ dom 𝑔) = dom 𝑏)
20	19	sseq1d 3595	. . . . . . . . . . 11 ⊢ ((𝑔 ↾ 𝑎) = 𝑏 → ((𝑎 ∩ dom 𝑔) ⊆ ∪ 𝑀 ↔ dom 𝑏 ⊆ ∪ 𝑀))
21	16, 20	syl5ibcom 234	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝑀 → ((𝑔 ↾ 𝑎) = 𝑏 → dom 𝑏 ⊆ ∪ 𝑀))
22	21	adantrd 483	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝑀 → (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) → dom 𝑏 ⊆ ∪ 𝑀))
23	22	rexlimiv 3009	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) → dom 𝑏 ⊆ ∪ 𝑀)
24	23	a1i 11	. . . . . . 7 ⊢ ((𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅) → (∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) → dom 𝑏 ⊆ ∪ 𝑀))
25	24	rexlimivv 3018	. . . . . 6 ⊢ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) → dom 𝑏 ⊆ ∪ 𝑀)
26	13, 25	sylbi 206	. . . . 5 ⊢ (𝑏 ∈ 𝑆 → dom 𝑏 ⊆ ∪ 𝑀)
27	5, 26	mprgbir 2911	. . . 4 ⊢ ∪ 𝑏 ∈ 𝑆 dom 𝑏 ⊆ ∪ 𝑀
28	27	a1i 11	. . 3 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∪ 𝑏 ∈ 𝑆 dom 𝑏 ⊆ ∪ 𝑀)
29		nofulllem5.1	. . . . . . . . 9 ⊢ 𝑀 = ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}
30	29	nofulllem4 31104	. . . . . . . 8 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → 𝑀 ∈ On)
31		eloni 5650	. . . . . . . 8 ⊢ (𝑀 ∈ On → Ord 𝑀)
32	30, 31	syl 17	. . . . . . 7 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → Ord 𝑀)
33		ordsucuniel 6916	. . . . . . 7 ⊢ (Ord 𝑀 → (𝑗 ∈ ∪ 𝑀 ↔ suc 𝑗 ∈ 𝑀))
34	32, 33	syl 17	. . . . . 6 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → (𝑗 ∈ ∪ 𝑀 ↔ suc 𝑗 ∈ 𝑀))
35		simpr 476	. . . . . . . 8 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → suc 𝑗 ∈ 𝑀)
36		onss 6882	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ On → 𝑀 ⊆ On)
37	30, 36	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → 𝑀 ⊆ On)
38	37	sselda 3568	. . . . . . . . . . 11 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → suc 𝑗 ∈ On)
39		ssrab2 3650	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} ⊆ On
40		onnmin 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} ⊆ On ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}) → ¬ suc 𝑗 ∈ ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)})
41	39, 40	mpan 702	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} → ¬ suc 𝑗 ∈ ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)})
42	41	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}) → ¬ suc 𝑗 ∈ ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)})
43	29	eleq2i 2680	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑗 ∈ 𝑀 ↔ suc 𝑗 ∈ ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)})
44	42, 43	sylnibr 318	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}) → ¬ suc 𝑗 ∈ 𝑀)
45	44	ex 449	. . . . . . . . . . . . . . 15 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} → ¬ suc 𝑗 ∈ 𝑀))
46	45	con2d 128	. . . . . . . . . . . . . 14 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → (suc 𝑗 ∈ 𝑀 → ¬ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}))
47	46	imp 444	. . . . . . . . . . . . 13 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → ¬ suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)})
48		reseq2 5312	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = suc 𝑗 → (𝑥 ↾ 𝑎) = (𝑥 ↾ suc 𝑗))
49		reseq2 5312	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = suc 𝑗 → (𝑦 ↾ 𝑎) = (𝑦 ↾ suc 𝑗))
50	48, 49	neeq12d 2843	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = suc 𝑗 → ((𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎) ↔ (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
51	50	2ralbidv 2972	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = suc 𝑗 → (∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎) ↔ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
52		reseq1 5311	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑔 → (𝑥 ↾ suc 𝑗) = (𝑔 ↾ suc 𝑗))
53	52	neeq1d 2841	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑔 → ((𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ (𝑔 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗)))
54		reseq1 5311	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ℎ → (𝑦 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗))
55	54	neeq2d 2842	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ℎ → ((𝑔 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗)))
56	53, 55	cbvral2v 3155	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ suc 𝑗) ≠ (𝑦 ↾ suc 𝑗) ↔ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
57	51, 56	syl6bb 275	. . . . . . . . . . . . . 14 ⊢ (𝑎 = suc 𝑗 → (∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎) ↔ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗)))
58	57	elrab 3331	. . . . . . . . . . . . 13 ⊢ (suc 𝑗 ∈ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)} ↔ (suc 𝑗 ∈ On ∧ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗)))
59	47, 58	sylnib 317	. . . . . . . . . . . 12 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → ¬ (suc 𝑗 ∈ On ∧ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗)))
60		imnan 437	. . . . . . . . . . . 12 ⊢ ((suc 𝑗 ∈ On → ¬ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗)) ↔ ¬ (suc 𝑗 ∈ On ∧ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗)))
61	59, 60	sylibr 223	. . . . . . . . . . 11 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → (suc 𝑗 ∈ On → ¬ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗)))
62	38, 61	mpd 15	. . . . . . . . . 10 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → ¬ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
63		df-ne 2782	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗) ↔ ¬ (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗))
64	63	con2bii 346	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ↔ ¬ (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
65	64	rexbii 3023	. . . . . . . . . . . . 13 ⊢ (∃ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ↔ ∃ℎ ∈ 𝑅 ¬ (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
66		rexnal 2978	. . . . . . . . . . . . 13 ⊢ (∃ℎ ∈ 𝑅 ¬ (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗) ↔ ¬ ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
67	65, 66	bitri 263	. . . . . . . . . . . 12 ⊢ (∃ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ↔ ¬ ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
68	67	rexbii 3023	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ↔ ∃𝑔 ∈ 𝐿 ¬ ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
69		rexnal 2978	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ 𝐿 ¬ ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗) ↔ ¬ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
70	68, 69	bitri 263	. . . . . . . . . 10 ⊢ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ↔ ¬ ∀𝑔 ∈ 𝐿 ∀ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) ≠ (ℎ ↾ suc 𝑗))
71	62, 70	sylibr 223	. . . . . . . . 9 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗))
72		simp3 1056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦)
73		breq1 4586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑔 → (𝑥 <s 𝑦 ↔ 𝑔 <s 𝑦))
74		breq2 4587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = ℎ → (𝑔 <s 𝑦 ↔ 𝑔 <s ℎ))
75	73, 74	rspc2v 3293	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅) → (∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦 → 𝑔 <s ℎ))
76	72, 75	mpan9 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅)) → 𝑔 <s ℎ)
77	76	adantrl 748	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → 𝑔 <s ℎ)
78		simp1l 1078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → 𝐿 ⊆ No )
79		simprl 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅)) → 𝑔 ∈ 𝐿)
80		ssel2 3563	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 ⊆ No ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ No )
81	78, 79, 80	syl2an 493	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → 𝑔 ∈ No )
82		sltirr 31069	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ No → ¬ 𝑔 <s 𝑔)
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ¬ 𝑔 <s 𝑔)
84		breq2 4587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = ℎ → (𝑔 <s 𝑔 ↔ 𝑔 <s ℎ))
85	84	biimprcd 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 <s ℎ → (𝑔 = ℎ → 𝑔 <s 𝑔))
86	85	con3d 147	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 <s ℎ → (¬ 𝑔 <s 𝑔 → ¬ 𝑔 = ℎ))
87	77, 83, 86	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ¬ 𝑔 = ℎ)
88	87	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗)) → ¬ 𝑔 = ℎ)
89		ioran 510	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ↔ (¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ℎ))
90		simp2l 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → 𝑅 ⊆ No )
91		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅)) → ℎ ∈ 𝑅)
92		ssel2 3563	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 ⊆ No ∧ ℎ ∈ 𝑅) → ℎ ∈ No )
93	90, 91, 92	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ℎ ∈ No )
94	93	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom ℎ) → ℎ ∈ No )
95		nofun 31046	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ∈ No → Fun ℎ)
96		funrel 5821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun ℎ → Rel ℎ)
97	94, 95, 96	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom ℎ) → Rel ℎ)
98	32	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → Ord 𝑀)
99		simprl 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → suc 𝑗 ∈ 𝑀)
100		ordelon 5664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Ord 𝑀 ∧ suc 𝑗 ∈ 𝑀) → suc 𝑗 ∈ On)
101	98, 99, 100	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → suc 𝑗 ∈ On)
102		sucelon 6909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ On ↔ suc 𝑗 ∈ On)
103	101, 102	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → 𝑗 ∈ On)
104		eloni 5650	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ On → Ord 𝑗)
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → Ord 𝑗)
106		nodmord 31050	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ ∈ No → Ord dom ℎ)
107	93, 106	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → Ord dom ℎ)
108		ordtri2or 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝑗 ∧ Ord dom ℎ) → (𝑗 ∈ dom ℎ ∨ dom ℎ ⊆ 𝑗))
109	105, 107, 108	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → (𝑗 ∈ dom ℎ ∨ dom ℎ ⊆ 𝑗))
110	109	orcanai 950	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom ℎ) → dom ℎ ⊆ 𝑗)
111		sssucid 5719	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑗 ⊆ suc 𝑗
112	110, 111	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom ℎ) → dom ℎ ⊆ suc 𝑗)
113		relssres 5357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel ℎ ∧ dom ℎ ⊆ suc 𝑗) → (ℎ ↾ suc 𝑗) = ℎ)
114	97, 112, 113	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom ℎ) → (ℎ ↾ suc 𝑗) = ℎ)
115	114	ex 449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → (¬ 𝑗 ∈ dom ℎ → (ℎ ↾ suc 𝑗) = ℎ))
116	81	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → 𝑔 ∈ No )
117		nofun 31046	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔 ∈ No → Fun 𝑔)
118		funrel 5821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun 𝑔 → Rel 𝑔)
119	116, 117, 118	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → Rel 𝑔)
120		nodmord 31050	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 ∈ No → Ord dom 𝑔)
121	81, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → Ord dom 𝑔)
122		ordtri2or 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝑗 ∧ Ord dom 𝑔) → (𝑗 ∈ dom 𝑔 ∨ dom 𝑔 ⊆ 𝑗))
123	105, 121, 122	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → (𝑗 ∈ dom 𝑔 ∨ dom 𝑔 ⊆ 𝑗))
124	123	orcanai 950	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → dom 𝑔 ⊆ 𝑗)
125	124, 111	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → dom 𝑔 ⊆ suc 𝑗)
126		relssres 5357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel 𝑔 ∧ dom 𝑔 ⊆ suc 𝑗) → (𝑔 ↾ suc 𝑗) = 𝑔)
127	119, 125, 126	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ ¬ 𝑗 ∈ dom 𝑔) → (𝑔 ↾ suc 𝑗) = 𝑔)
128	127	ex 449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → (¬ 𝑗 ∈ dom 𝑔 → (𝑔 ↾ suc 𝑗) = 𝑔))
129	115, 128	anim12d 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ((¬ 𝑗 ∈ dom ℎ ∧ ¬ 𝑗 ∈ dom 𝑔) → ((ℎ ↾ suc 𝑗) = ℎ ∧ (𝑔 ↾ suc 𝑗) = 𝑔)))
130	129	ancomsd 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ℎ) → ((ℎ ↾ suc 𝑗) = ℎ ∧ (𝑔 ↾ suc 𝑗) = 𝑔)))
131		eqeq12 2623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 ↾ suc 𝑗) = 𝑔 ∧ (ℎ ↾ suc 𝑗) = ℎ) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ↔ 𝑔 = ℎ))
132	131	biimpd 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔 ↾ suc 𝑗) = 𝑔 ∧ (ℎ ↾ suc 𝑗) = ℎ) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → 𝑔 = ℎ))
133	132	ancoms 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ ↾ suc 𝑗) = ℎ ∧ (𝑔 ↾ suc 𝑗) = 𝑔) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → 𝑔 = ℎ))
134	130, 133	syl6 34	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ℎ) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → 𝑔 = ℎ)))
135	134	com23 84	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ℎ) → 𝑔 = ℎ)))
136	135	imp 444	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗)) → ((¬ 𝑗 ∈ dom 𝑔 ∧ ¬ 𝑗 ∈ dom ℎ) → 𝑔 = ℎ))
137	89, 136	syl5bi 231	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗)) → (¬ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) → 𝑔 = ℎ))
138	88, 137	mt3d 139	. . . . . . . . . . . . . . 15 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) ∧ (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗)) → (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ))
139	138	ex 449	. . . . . . . . . . . . . 14 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ (suc 𝑗 ∈ 𝑀 ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅))) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ)))
140	139	anassrs 678	. . . . . . . . . . . . 13 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) ∧ (𝑔 ∈ 𝐿 ∧ ℎ ∈ 𝑅)) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ)))
141	140	anassrs 678	. . . . . . . . . . . 12 ⊢ ((((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) ∧ 𝑔 ∈ 𝐿) ∧ ℎ ∈ 𝑅) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ)))
142	141	ancld 574	. . . . . . . . . . 11 ⊢ ((((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) ∧ 𝑔 ∈ 𝐿) ∧ ℎ ∈ 𝑅) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ))))
143	142	reximdva 3000	. . . . . . . . . 10 ⊢ (((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) ∧ 𝑔 ∈ 𝐿) → (∃ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → ∃ℎ ∈ 𝑅 ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ))))
144	143	reximdva 3000	. . . . . . . . 9 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) → ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ))))
145	71, 144	mpd 15	. . . . . . . 8 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ)))
146		reseq2 5312	. . . . . . . . . . . . 13 ⊢ (𝑎 = suc 𝑗 → (𝑔 ↾ 𝑎) = (𝑔 ↾ suc 𝑗))
147		reseq2 5312	. . . . . . . . . . . . 13 ⊢ (𝑎 = suc 𝑗 → (ℎ ↾ 𝑎) = (ℎ ↾ suc 𝑗))
148	146, 147	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ (𝑎 = suc 𝑗 → ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ↔ (𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗)))
149		eleq2 2677	. . . . . . . . . . . 12 ⊢ (𝑎 = suc 𝑗 → (𝑗 ∈ 𝑎 ↔ 𝑗 ∈ suc 𝑗))
150	148, 149	3anbi13d 1393	. . . . . . . . . . 11 ⊢ (𝑎 = suc 𝑗 → (((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ suc 𝑗)))
151		vex 3176	. . . . . . . . . . . . 13 ⊢ 𝑗 ∈ V
152	151	sucid 5721	. . . . . . . . . . . 12 ⊢ 𝑗 ∈ suc 𝑗
153		df-3an 1033	. . . . . . . . . . . 12 ⊢ (((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ suc 𝑗) ↔ (((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ)) ∧ 𝑗 ∈ suc 𝑗))
154	152, 153	mpbiran2 956	. . . . . . . . . . 11 ⊢ (((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ suc 𝑗) ↔ ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ)))
155	150, 154	syl6bb 275	. . . . . . . . . 10 ⊢ (𝑎 = suc 𝑗 → (((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ))))
156	155	2rexbidv 3039	. . . . . . . . 9 ⊢ (𝑎 = suc 𝑗 → (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ))))
157	156	rspcev 3282	. . . . . . . 8 ⊢ ((suc 𝑗 ∈ 𝑀 ∧ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ suc 𝑗) = (ℎ ↾ suc 𝑗) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ))) → ∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
158	35, 145, 157	syl2anc 691	. . . . . . 7 ⊢ ((((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) ∧ suc 𝑗 ∈ 𝑀) → ∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
159	158	ex 449	. . . . . 6 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → (suc 𝑗 ∈ 𝑀 → ∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎)))
160	34, 159	sylbid 229	. . . . 5 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → (𝑗 ∈ ∪ 𝑀 → ∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎)))
161		eliun 4460	. . . . . 6 ⊢ (𝑗 ∈ ∪ 𝑏 ∈ 𝑆 dom 𝑏 ↔ ∃𝑏 ∈ 𝑆 𝑗 ∈ dom 𝑏)
162	12	rexeqi 3120	. . . . . 6 ⊢ (∃𝑏 ∈ 𝑆 𝑗 ∈ dom 𝑏 ↔ ∃𝑏 ∈ {𝑓 ∣ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓)}𝑗 ∈ dom 𝑏)
163		r19.41vv 3072	. . . . . . . . . 10 ⊢ (∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
164	163	rexbii 3023	. . . . . . . . 9 ⊢ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑔 ∈ 𝐿 (∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
165		r19.41v 3070	. . . . . . . . 9 ⊢ (∃𝑔 ∈ 𝐿 (∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
166	164, 165	bitri 263	. . . . . . . 8 ⊢ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
167	166	exbii 1764	. . . . . . 7 ⊢ (∃𝑏∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏(∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
168		rexcom 3080	. . . . . . . . 9 ⊢ (∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑔 ∈ 𝐿 ∃𝑎 ∈ 𝑀 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
169		rexcom 3080	. . . . . . . . . 10 ⊢ (∃𝑎 ∈ 𝑀 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
170	169	rexbii 3023	. . . . . . . . 9 ⊢ (∃𝑔 ∈ 𝐿 ∃𝑎 ∈ 𝑀 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
171	168, 170	bitri 263	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
172		vex 3176	. . . . . . . . . . . . . . . 16 ⊢ ℎ ∈ V
173	172	resex 5363	. . . . . . . . . . . . . . 15 ⊢ (ℎ ↾ 𝑎) ∈ V
174		eqeq2 2621	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (ℎ ↾ 𝑎) → ((𝑔 ↾ 𝑎) = 𝑏 ↔ (𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎)))
175		dmeq 5246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (ℎ ↾ 𝑎) → dom 𝑏 = dom (ℎ ↾ 𝑎))
176	175	eleq2d 2673	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (ℎ ↾ 𝑎) → (𝑗 ∈ dom 𝑏 ↔ 𝑗 ∈ dom (ℎ ↾ 𝑎)))
177	174, 176	anbi12d 743	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (ℎ ↾ 𝑎) → (((𝑔 ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏) ↔ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ 𝑗 ∈ dom (ℎ ↾ 𝑎))))
178	173, 177	ceqsexv 3215	. . . . . . . . . . . . . 14 ⊢ (∃𝑏(𝑏 = (ℎ ↾ 𝑎) ∧ ((𝑔 ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)) ↔ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ 𝑗 ∈ dom (ℎ ↾ 𝑎)))
179		an12 834	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ ↾ 𝑎) = 𝑏 ∧ ((𝑔 ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)) ↔ ((𝑔 ↾ 𝑎) = 𝑏 ∧ ((ℎ ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)))
180		eqcom 2617	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (ℎ ↾ 𝑎) ↔ (ℎ ↾ 𝑎) = 𝑏)
181	180	anbi1i 727	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 = (ℎ ↾ 𝑎) ∧ ((𝑔 ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)) ↔ ((ℎ ↾ 𝑎) = 𝑏 ∧ ((𝑔 ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)))
182		anass 679	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ((𝑔 ↾ 𝑎) = 𝑏 ∧ ((ℎ ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)))
183	179, 181, 182	3bitr4i 291	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = (ℎ ↾ 𝑎) ∧ ((𝑔 ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)) ↔ (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
184	183	exbii 1764	. . . . . . . . . . . . . 14 ⊢ (∃𝑏(𝑏 = (ℎ ↾ 𝑎) ∧ ((𝑔 ↾ 𝑎) = 𝑏 ∧ 𝑗 ∈ dom 𝑏)) ↔ ∃𝑏(((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
185		dmeq 5246	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) → dom (𝑔 ↾ 𝑎) = dom (ℎ ↾ 𝑎))
186	185	eleq2d 2673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) → (𝑗 ∈ dom (𝑔 ↾ 𝑎) ↔ 𝑗 ∈ dom (ℎ ↾ 𝑎)))
187	186	orbi1d 735	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) → ((𝑗 ∈ dom (𝑔 ↾ 𝑎) ∨ 𝑗 ∈ dom (ℎ ↾ 𝑎)) ↔ (𝑗 ∈ dom (ℎ ↾ 𝑎) ∨ 𝑗 ∈ dom (ℎ ↾ 𝑎))))
188		oridm 535	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ dom (ℎ ↾ 𝑎) ∨ 𝑗 ∈ dom (ℎ ↾ 𝑎)) ↔ 𝑗 ∈ dom (ℎ ↾ 𝑎))
189	187, 188	syl6rbb 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) → (𝑗 ∈ dom (ℎ ↾ 𝑎) ↔ (𝑗 ∈ dom (𝑔 ↾ 𝑎) ∨ 𝑗 ∈ dom (ℎ ↾ 𝑎))))
190		incom 3767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∩ dom 𝑔) = (dom 𝑔 ∩ 𝑎)
191	17, 190	eqtri 2632	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑔 ↾ 𝑎) = (dom 𝑔 ∩ 𝑎)
192	191	elin2 3763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ dom (𝑔 ↾ 𝑎) ↔ (𝑗 ∈ dom 𝑔 ∧ 𝑗 ∈ 𝑎))
193		dmres 5339	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (ℎ ↾ 𝑎) = (𝑎 ∩ dom ℎ)
194		incom 3767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∩ dom ℎ) = (dom ℎ ∩ 𝑎)
195	193, 194	eqtri 2632	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (ℎ ↾ 𝑎) = (dom ℎ ∩ 𝑎)
196	195	elin2 3763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ dom (ℎ ↾ 𝑎) ↔ (𝑗 ∈ dom ℎ ∧ 𝑗 ∈ 𝑎))
197	192, 196	orbi12i 542	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ dom (𝑔 ↾ 𝑎) ∨ 𝑗 ∈ dom (ℎ ↾ 𝑎)) ↔ ((𝑗 ∈ dom 𝑔 ∧ 𝑗 ∈ 𝑎) ∨ (𝑗 ∈ dom ℎ ∧ 𝑗 ∈ 𝑎)))
198		andir 908	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ((𝑗 ∈ dom 𝑔 ∧ 𝑗 ∈ 𝑎) ∨ (𝑗 ∈ dom ℎ ∧ 𝑗 ∈ 𝑎)))
199	197, 198	bitr4i 266	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ dom (𝑔 ↾ 𝑎) ∨ 𝑗 ∈ dom (ℎ ↾ 𝑎)) ↔ ((𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
200	189, 199	syl6bb 275	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) → (𝑗 ∈ dom (ℎ ↾ 𝑎) ↔ ((𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎)))
201	200	pm5.32i 667	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ 𝑗 ∈ dom (ℎ ↾ 𝑎)) ↔ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ ((𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎)))
202		3anass 1035	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ ((𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎)))
203	201, 202	bitr4i 266	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ 𝑗 ∈ dom (ℎ ↾ 𝑎)) ↔ ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
204	178, 184, 203	3bitr3ri 290	. . . . . . . . . . . . 13 ⊢ (((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑏(((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
205	204	rexbii 3023	. . . . . . . . . . . 12 ⊢ (∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑎 ∈ 𝑀 ∃𝑏(((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
206		rexcom4 3198	. . . . . . . . . . . 12 ⊢ (∃𝑎 ∈ 𝑀 ∃𝑏(((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
207	205, 206	bitri 263	. . . . . . . . . . 11 ⊢ (∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑏∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
208	207	rexbii 3023	. . . . . . . . . 10 ⊢ (∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃ℎ ∈ 𝑅 ∃𝑏∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
209		rexcom4 3198	. . . . . . . . . 10 ⊢ (∃ℎ ∈ 𝑅 ∃𝑏∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
210	208, 209	bitri 263	. . . . . . . . 9 ⊢ (∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑏∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
211	210	rexbii 3023	. . . . . . . 8 ⊢ (∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑔 ∈ 𝐿 ∃𝑏∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
212		rexcom4 3198	. . . . . . . 8 ⊢ (∃𝑔 ∈ 𝐿 ∃𝑏∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏) ↔ ∃𝑏∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
213	171, 211, 212	3bitri 285	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎) ↔ ∃𝑏∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 (((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
214	11	rexab 3336	. . . . . . 7 ⊢ (∃𝑏 ∈ {𝑓 ∣ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓)}𝑗 ∈ dom 𝑏 ↔ ∃𝑏(∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑏 ∧ (ℎ ↾ 𝑎) = 𝑏) ∧ 𝑗 ∈ dom 𝑏))
215	167, 213, 214	3bitr4ri 292	. . . . . 6 ⊢ (∃𝑏 ∈ {𝑓 ∣ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓)}𝑗 ∈ dom 𝑏 ↔ ∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
216	161, 162, 215	3bitri 285	. . . . 5 ⊢ (𝑗 ∈ ∪ 𝑏 ∈ 𝑆 dom 𝑏 ↔ ∃𝑎 ∈ 𝑀 ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ((𝑔 ↾ 𝑎) = (ℎ ↾ 𝑎) ∧ (𝑗 ∈ dom 𝑔 ∨ 𝑗 ∈ dom ℎ) ∧ 𝑗 ∈ 𝑎))
217	160, 216	syl6ibr 241	. . . 4 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → (𝑗 ∈ ∪ 𝑀 → 𝑗 ∈ ∪ 𝑏 ∈ 𝑆 dom 𝑏))
218	217	ssrdv 3574	. . 3 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∪ 𝑀 ⊆ ∪ 𝑏 ∈ 𝑆 dom 𝑏)
219	28, 218	eqssd 3585	. 2 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∪ 𝑏 ∈ 𝑆 dom 𝑏 = ∪ 𝑀)
220	4, 219	syl5eq 2656	1 ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → dom 𝑋 = ∪ 𝑀)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ∩ cin 3539   ⊆ wss 3540  ∪ cuni 4372  ∩ cint 4410  ∪ ciun 4455   class class class wbr 4583  dom cdm 5038   ↾ cres 5040  Rel wrel 5043  Ord word 5639  Oncon0 5640  suc csuc 5642  Fun wfun 5798   No csur 31037   <s cslt 31038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-1o 7447  df-2o 7448  df-no 31040  df-slt 31041  df-bday 31042

This theorem is referenced by: (None)