Theorem fpwwe2lem11 10726

Description: Lemma for fpwwe2 10728. (Contributed by Mario Carneiro, 18-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.)

Hypotheses

Ref	Expression
fpwwe2.1	⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2	⊢ (𝜑 → 𝐴 ∈ 𝑉)
fpwwe2.3	⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2.4	⊢ 𝑋 = ∪ dom 𝑊

Assertion

Ref	Expression
fpwwe2lem11	⊢ (𝜑 → 𝑋 ∈ dom 𝑊)

Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑊,𝑟,𝑢,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑦, 𝑢)   𝑉(𝑥, 𝑦, 𝑢, 𝑟)

Proof of Theorem fpwwe2lem11

Dummy variables 𝑎 𝑏 𝑠 𝑡 𝑣 𝑤 𝑧 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fpwwe2.4	. . . . 5 ⊢ 𝑋 = ∪ dom 𝑊
2		vex 3455	. . . . . . . . 9 ⊢ 𝑎 ∈ V
3	2	eldm 5882	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5		fpwwe2.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
6	4, 5	fpwwe2lem2 10717	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
7	6	simprbda 504	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)))
8	7	simpld 500	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝐴)
9		velpw 4562	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝒫 𝐴 ↔ 𝑎 ⊆ 𝐴)
10	8, 9	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
11	10	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
12	11	exlimdv 1966	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
13	3, 12	biimtrid 245	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → 𝑎 ∈ 𝒫 𝐴))
14	13	ssrdv 3937	. . . . . 6 ⊢ (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15		sspwuni 5060	. . . . . 6 ⊢ (dom 𝑊 ⊆ 𝒫 𝐴 ↔ ∪ dom 𝑊 ⊆ 𝐴)
16	14, 15	sylib 221	. . . . 5 ⊢ (𝜑 → ∪ dom 𝑊 ⊆ 𝐴)
17	1, 16	eqsstrid 3969	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
18		vex 3455	. . . . . . . 8 ⊢ 𝑠 ∈ V
19	18	elrn 5875	. . . . . . 7 ⊢ (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
20	7	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
21	4	relopabiv 5798	. . . . . . . . . . . . . . . 16 ⊢ Rel 𝑊
22	21	releldmi 5930	. . . . . . . . . . . . . . 15 ⊢ (𝑎𝑊𝑠 → 𝑎 ∈ dom 𝑊)
23	22	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24		elssuni 4899	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑊 → 𝑎 ⊆ ∪ dom 𝑊)
25	23, 24	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ ∪ dom 𝑊)
26	25, 1	sseqtrrdi 3972	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝑋)
27		xpss12 5666	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
28	26, 26, 27	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
29	20, 28	sstrd 3941	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30		velpw 4562	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
31	29, 30	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
32	31	ex 418	. . . . . . . 8 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
33	32	exlimdv 1966	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
34	19, 33	biimtrid 245	. . . . . 6 ⊢ (𝜑 → (𝑠 ∈ ran 𝑊 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
35	34	ssrdv 3937	. . . . 5 ⊢ (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36		sspwuni 5060	. . . . 5 ⊢ (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
37	35, 36	sylib 221	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
38	17, 37	jca 521	. . 3 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)))
39		n0 4300	. . . . . . . . 9 ⊢ (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑛)
40		ssel2 3926	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛) → 𝑦 ∈ 𝑋)
41	40	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → 𝑦 ∈ 𝑋)
42	1	eleq2i 2853	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ dom 𝑊)
43		eluni2 4871	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∪ dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
44	42, 43	bitri 278	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
45	41, 44	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
46	2	inex2 5278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ∈ V
47	46	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ∈ V)
48	6	simplbda 505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
49	48	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 We 𝑎)
50	49	ad2ant2r 760	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 We 𝑎)
51		wefr 5641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 We 𝑎 → 𝑠 Fr 𝑎)
52	50, 51	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 Fr 𝑎)
53		inss2 4183	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ⊆ 𝑎
54	53	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ⊆ 𝑎)
55		simplrr 790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑛)
56		simprr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑎)
57		inelcm 4418	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑛 ∧ 𝑦 ∈ 𝑎) → (𝑛 ∩ 𝑎) ≠ ∅)
58	55, 56, 57	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ≠ ∅)
59		fri 5609	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∩ 𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛 ∩ 𝑎) ⊆ 𝑎 ∧ (𝑛 ∩ 𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
60	47, 52, 54, 58, 59	syl22anc 852	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
61		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛 ∩ 𝑎))
62	61	elin1d 4150	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑛)
63		simplrr 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
64		ralnex 3089	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
65	63, 64	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
66		df-br 5104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊)
67		eluni2 4871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
68	66, 67	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
69		vex 3455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑡 ∈ V
70	69	elrn 5875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
71		df-br 5104	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
72		simprll 791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑛)
73	72	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑛)
74		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣)
75		simp-4l 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑)
76		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑎𝑊𝑠)
77	76	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠)
78		simprlr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡)
79		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑏𝑊𝑡)
80	4, 5	fpwwe2lem2 10717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
81	80	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
82	79, 81	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
83	82	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)))
84	83	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
85	75, 77, 78, 84	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
86	85	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣 → 𝑤(𝑏 × 𝑏)𝑣))
87	74, 86	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
88		brxp 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑏))
89	88	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤(𝑏 × 𝑏)𝑣 → 𝑤 ∈ 𝑏)
90	87, 89	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑏)
91	90	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
92	61	elin2d 4151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑎)
93	92	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣 ∈ 𝑎)
94		simplrr 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
95		brinxp2 5729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑎) ∧ 𝑤𝑡𝑣))
96	91, 93, 94, 95	syl21anbrc 1363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
97		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
98	97	breqd 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 ↔ 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
99	96, 98	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
100	75, 77, 20	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
101	100	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
102	101	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 → 𝑤(𝑎 × 𝑎)𝑣))
103	99, 102	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
104		brxp 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤 ∈ 𝑎 ∧ 𝑣 ∈ 𝑎))
105	104	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤(𝑎 × 𝑎)𝑣 → 𝑤 ∈ 𝑎)
106	103, 105	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
107	73, 106	elind 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
108		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑤 → (𝑧𝑠𝑣 ↔ 𝑤𝑠𝑣))
109	108	rspcev 3577	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ (𝑛 ∩ 𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
110	107, 99, 109	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
111	72	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑛)
112		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎)
113	90	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏)
114	112, 113	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
115	111, 114	elind 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
116		simplrr 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
117		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
118		inss1 4182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
119	117, 118	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
120	119	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣 → 𝑤𝑠𝑣))
121	116, 120	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
122	115, 121, 109	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
123	5	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝐴 ∈ 𝑉)
124		fpwwe2.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
125	124	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
127	4, 123, 125, 126, 79	fpwwe2lem9 10724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
128	75, 77, 78, 127	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
129	110, 122, 128	mpjaodan 973	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
130	129	expr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
131	71, 130	biimtrrid 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
132	131	expr 462	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
133	132	exlimdv 1966	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
134	70, 133	biimtrid 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
135	134	rexlimdv 3162	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
136	68, 135	biimtrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑤∪ ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
137	65, 136	mtod 201	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ 𝑤∪ ran 𝑊 𝑣)
138	137	ralrimiva 3155	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
139	60, 62, 138	reximssdv 3181	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
140	139	exp32 426	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
141	140	exlimdv 1966	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
142	3, 141	biimtrid 245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
143	142	rexlimdv 3162	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
144	45, 143	mpd 16	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
145	144	expr 462	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
146	145	exlimdv 1966	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (∃𝑦 𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
147	39, 146	biimtrid 245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑛 ≠ ∅ → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
148	147	expimpd 459	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
149	148	alrimiv 1960	. . . . . 6 ⊢ (𝜑 → ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
150		df-fr 5604	. . . . . 6 ⊢ (∪ ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
151	149, 150	sylibr 237	. . . . 5 ⊢ (𝜑 → ∪ ran 𝑊 Fr 𝑋)
152	1	eleq2i 2853	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑋 ↔ 𝑤 ∈ ∪ dom 𝑊)
153		eluni2 4871	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
154	152, 153	bitri 278	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
155	44, 154	anbi12i 640	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
156		reeanv 3235	. . . . . . . 8 ⊢ (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
157	155, 156	bitr4i 281	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ ∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏))
158		vex 3455	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
159	158	eldm 5882	. . . . . . . . . . 11 ⊢ (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
160	3, 159	anbi12i 640	. . . . . . . . . 10 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
161		exdistrv 1988	. . . . . . . . . 10 ⊢ (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
162	160, 161	bitr4i 281	. . . . . . . . 9 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ ∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡))
163	82	simprd 501	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
164	163	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 We 𝑏)
165	164	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
166		weso 5642	. . . . . . . . . . . . . . 15 ⊢ (𝑡 We 𝑏 → 𝑡 Or 𝑏)
167	165, 166	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
168		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎 ⊆ 𝑏)
169		simplrl 789	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑎)
170	168, 169	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑏)
171		simplrr 790	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
172		solin 5586	. . . . . . . . . . . . . 14 ⊢ ((𝑡 Or 𝑏 ∧ (𝑦 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏)) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
173	167, 170, 171, 172	syl12anc 850	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
174	21	relelrni 5931	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏𝑊𝑡 → 𝑡 ∈ ran 𝑊)
175	174	ad2antll 742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
176	175	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
177		elssuni 4899	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ran 𝑊 → 𝑡 ⊆ ∪ ran 𝑊)
178	176, 177	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ ∪ ran 𝑊)
179	178	ssbrd 5148	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 → 𝑦∪ ran 𝑊 𝑤))
180		idd 25	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
181	178	ssbrd 5148	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦 → 𝑤∪ ran 𝑊 𝑦))
182	179, 180, 181	3orim123d 1472	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
183	173, 182	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
184	49	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 We 𝑎)
185	184	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
186		weso 5642	. . . . . . . . . . . . . . 15 ⊢ (𝑠 We 𝑎 → 𝑠 Or 𝑎)
187	185, 186	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
188		simplrl 789	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦 ∈ 𝑎)
189		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎)
190		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏)
191	189, 190	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
192		solin 5586	. . . . . . . . . . . . . 14 ⊢ ((𝑠 Or 𝑎 ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
193	187, 188, 191, 192	syl12anc 850	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
194	21	relelrni 5931	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑊𝑠 → 𝑠 ∈ ran 𝑊)
195	194	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
196	195	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
197		elssuni 4899	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ran 𝑊 → 𝑠 ⊆ ∪ ran 𝑊)
198	196, 197	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ⊆ ∪ ran 𝑊)
199	198	ssbrd 5148	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 → 𝑦∪ ran 𝑊 𝑤))
200		idd 25	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
201	198	ssbrd 5148	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦 → 𝑤∪ ran 𝑊 𝑦))
202	199, 200, 201	3orim123d 1472	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
203	193, 202	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
204	127	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
205	183, 203, 204	mpjaodan 973	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
206	205	exp31 425	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
207	206	exlimdvv 1967	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
208	162, 207	biimtrid 245	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
209	208	rexlimdvv 3219	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
210	157, 209	biimtrid 245	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
211	210	ralrimivv 3204	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
212		dfwe2 7788	. . . . 5 ⊢ (∪ ran 𝑊 We 𝑋 ↔ (∪ ran 𝑊 Fr 𝑋 ∧ ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
213	151, 211, 212	sylanbrc 595	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 We 𝑋)
214	4	fpwwe2cbv 10715	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤 ∈ 𝑧 [(◡𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
215	5	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝐴 ∈ 𝑉)
216		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎𝑊𝑠)
217	214, 215, 216	fpwwe2lem3 10718	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎𝑊𝑠) ∧ 𝑦 ∈ 𝑎) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
218	217	anasss 472	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
219		cnvimass 6198	. . . . . . . . . . . . 13 ⊢ (◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊
220	5, 17	ssexd 5286	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ V)
221	220, 220	xpexd 7765	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 × 𝑋) ∈ V)
222	221, 37	ssexd 5286	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ ran 𝑊 ∈ V)
223	222	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∪ ran 𝑊 ∈ V)
224	223	dmexd 7915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → dom ∪ ran 𝑊 ∈ V)
225		ssexg 5281	. . . . . . . . . . . . 13 ⊢ (((◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊 ∧ dom ∪ ran 𝑊 ∈ V) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
226	219, 224, 225	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
227		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (◡∪ ran 𝑊 “ {𝑦}) → 𝑢 = (◡∪ ran 𝑊 “ {𝑦}))
228		olc 882	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
229		df-br 5104	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊)
230		eluni2 4871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
231	229, 230	bitri 278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
232		df-br 5104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
233	84	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
234	233	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑏)𝑤))
235		brxp 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏))
236	235	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑧(𝑏 × 𝑏)𝑤 → 𝑧 ∈ 𝑏)
237	234, 236	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧 ∈ 𝑏))
238	20	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
239	238	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑤𝑠𝑦 → 𝑤(𝑎 × 𝑎)𝑦))
240	239	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
241		brxp 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎))
242	241	simplbi 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤(𝑎 × 𝑎)𝑦 → 𝑤 ∈ 𝑎)
243	240, 242	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤 ∈ 𝑎)
244	243	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
245		elequ1 2152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎))
246	245	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑤 = 𝑦 → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
247	246	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
248	244, 247	jaodan 972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
249	248	impr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → 𝑤 ∈ 𝑎)
250	249	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
251	237, 250	jctird 536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎)))
252		brxp 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎))
253	251, 252	imbitrrdi 255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑎)𝑤))
254	253	ancld 560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
255		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
256	255	breqd 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ 𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
257		brin 5157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤))
258	256, 257	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
259	254, 258	sylibrd 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
260		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
261	260, 118	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
262	261	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
263	127	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
264	259, 262, 263	mpjaodan 973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
265	232, 264	biimtrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
266	265	exp32 426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
267	266	expr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
268	267	com24 96	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑦 ∈ 𝑎 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
269	268	impr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
270	269	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
271	270	exlimdv 1966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
272	70, 271	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
273	272	rexlimdv 3162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
274	231, 273	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
275	228, 274	sylan2 605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤 = 𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
276	275	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
277	276	alrimiv 1960	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
278		breq2 5107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧∪ ran 𝑊 𝑦))
279		breq2 5107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧𝑠𝑤 ↔ 𝑧𝑠𝑦))
280	278, 279	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑦 → ((𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦)))
281	280	equsalvw 2037	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
282	277, 281	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
283	194	ad2antrl 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ∈ ran 𝑊)
284	283, 197	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ⊆ ∪ ran 𝑊)
285	284	ssbrd 5148	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑠𝑦 → 𝑧∪ ran 𝑊 𝑦))
286	282, 285	impbid 215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 ↔ 𝑧𝑠𝑦))
287		vex 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ V
288	287	eliniseg 6092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦))
289	288	elv 3456	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦)
290	287	eliniseg 6092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
291	290	elv 3456	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
292	286, 289, 291	3bitr4g 317	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (◡𝑠 “ {𝑦})))
293	292	eqrdv 2759	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) = (◡𝑠 “ {𝑦}))
294	227, 293	sylan9eqr 2818	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → 𝑢 = (◡𝑠 “ {𝑦}))
295	294	sqxpeqd 5683	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
296	295	ineq2d 4166	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
297		relinxp 5792	. . . . . . . . . . . . . . . . 17 ⊢ Rel (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
298		relinxp 5792	. . . . . . . . . . . . . . . . 17 ⊢ Rel (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
299		vex 3455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
300	299	eliniseg 6092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ V → (𝑤 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
301	290, 300	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ V → ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)))
302	301	elv 3456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦))
303		orc 881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤𝑠𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
304	303, 274	sylan2 605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
305	304	adantrl 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
306	284	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → 𝑠 ⊆ ∪ ran 𝑊)
307	306	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧𝑠𝑤 → 𝑧∪ ran 𝑊 𝑤))
308	305, 307	impbid 215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
309	302, 308	sylan2b 606	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦}))) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
310	309	pm5.32da 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
311		df-br 5104	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
312		brinxp2 5729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
313	311, 312	bitr3i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
314		df-br 5104	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
315		brinxp2 5729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
316	314, 315	bitr3i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
317	310, 313, 316	3bitr4g 317	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
318	297, 298, 317	eqrelrdv 5768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
319	318	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
320	296, 319	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
321	294, 320	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
322	321	eqeq1d 2763	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → ((𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
323	226, 322	sbcied 3782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ([(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
324	218, 323	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
325	324	exp32 426	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
326	325	exlimdv 1966	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
327	3, 326	biimtrid 245	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
328	327	rexlimdv 3162	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
329	44, 328	biimtrid 245	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝑋 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
330	329	ralrimiv 3154	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
331	213, 330	jca 521	. . 3 ⊢ (𝜑 → (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
332	4, 5	fpwwe2lem2 10717	. . 3 ⊢ (𝜑 → (𝑋𝑊∪ ran 𝑊 ↔ ((𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
333	38, 331, 332	mpbir2and 726	. 2 ⊢ (𝜑 → 𝑋𝑊∪ ran 𝑊)
334	21	releldmi 5930	. 2 ⊢ (𝑋𝑊∪ ran 𝑊 → 𝑋 ∈ dom 𝑊)
335	333, 334	syl 18	1 ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451  [wsbc 3739   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ⟨cop 4590  ∪ cuni 4867   class class class wbr 5103  {copab 5167   Or wor 5558   Fr wfr 5601   We wwe 5603   × cxp 5649  ^◡ccnv 5650  dom cdm 5651  ran crn 5652   “ cima 5654  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-oi 9504

This theorem is used by:  fpwwe2lem12  10727  fpwwe2  10728