Theorem fpwwe2lem12 10052

Description: Lemma for fpwwe2 10054. (Contributed by Mario Carneiro, 18-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.)

Hypotheses

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

Assertion

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

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

Allowed substitution hints:   𝐴(𝑦,𝑢)

Proof of Theorem fpwwe2lem12

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

Step	Hyp	Ref	Expression
1		fpwwe2.4	. . . . 5 ⊢ 𝑋 = ∪ dom 𝑊
2		vex 3444	. . . . . . . . 9 ⊢ 𝑎 ∈ V
3	2	eldm 5733	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5		fpwwe2.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ V)
6	4, 5	fpwwe2lem2 10043	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
7	6	simprbda 502	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)))
8	7	simpld 498	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝐴)
9		velpw 4502	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝒫 𝐴 ↔ 𝑎 ⊆ 𝐴)
10	8, 9	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
11	10	ex 416	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
12	11	exlimdv 1934	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
13	3, 12	syl5bi 245	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → 𝑎 ∈ 𝒫 𝐴))
14	13	ssrdv 3921	. . . . . 6 ⊢ (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15		sspwuni 4985	. . . . . 6 ⊢ (dom 𝑊 ⊆ 𝒫 𝐴 ↔ ∪ dom 𝑊 ⊆ 𝐴)
16	14, 15	sylib 221	. . . . 5 ⊢ (𝜑 → ∪ dom 𝑊 ⊆ 𝐴)
17	1, 16	eqsstrid 3963	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
18		vex 3444	. . . . . . . 8 ⊢ 𝑠 ∈ V
19	18	elrn 5786	. . . . . . 7 ⊢ (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
20	7	simprd 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
21	4	relopabi 5658	. . . . . . . . . . . . . . . 16 ⊢ Rel 𝑊
22	21	releldmi 5782	. . . . . . . . . . . . . . 15 ⊢ (𝑎𝑊𝑠 → 𝑎 ∈ dom 𝑊)
23	22	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24		elssuni 4830	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑊 → 𝑎 ⊆ ∪ dom 𝑊)
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ ∪ dom 𝑊)
26	25, 1	sseqtrrdi 3966	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝑋)
27		xpss12 5534	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
28	26, 26, 27	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
29	20, 28	sstrd 3925	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30		velpw 4502	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
31	29, 30	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
32	31	ex 416	. . . . . . . 8 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
33	32	exlimdv 1934	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
34	19, 33	syl5bi 245	. . . . . 6 ⊢ (𝜑 → (𝑠 ∈ ran 𝑊 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
35	34	ssrdv 3921	. . . . 5 ⊢ (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36		sspwuni 4985	. . . . 5 ⊢ (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
37	35, 36	sylib 221	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
38	17, 37	jca 515	. . 3 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)))
39		n0 4260	. . . . . . . . 9 ⊢ (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑛)
40		ssel2 3910	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛) → 𝑦 ∈ 𝑋)
41	40	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → 𝑦 ∈ 𝑋)
42	1	eleq2i 2881	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ dom 𝑊)
43		eluni2 4804	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∪ dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
44	42, 43	bitri 278	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
45	41, 44	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
46	2	inex2 5186	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ∈ V
47	46	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ∈ V)
48	6	simplbda 503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
49	48	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 We 𝑎)
50	49	ad2ant2r 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 We 𝑎)
51		wefr 5509	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 We 𝑎 → 𝑠 Fr 𝑎)
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 Fr 𝑎)
53		inss2 4156	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ⊆ 𝑎
54	53	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ⊆ 𝑎)
55		simplrr 777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑛)
56		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑎)
57		inelcm 4372	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑛 ∧ 𝑦 ∈ 𝑎) → (𝑛 ∩ 𝑎) ≠ ∅)
58	55, 56, 57	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ≠ ∅)
59		fri 5481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∩ 𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛 ∩ 𝑎) ⊆ 𝑎 ∧ (𝑛 ∩ 𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
60	47, 52, 54, 58, 59	syl22anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
61		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛 ∩ 𝑎))
62	61	elin1d 4125	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑛)
63		simplrr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
64		ralnex 3199	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
65	63, 64	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
66		df-br 5031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊)
67		eluni2 4804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
68	66, 67	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
69		vex 3444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑡 ∈ V
70	69	elrn 5786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
71		df-br 5031	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
72		simprll 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑛)
73	72	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑛)
74		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣)
75		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑)
76		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑎𝑊𝑠)
77	76	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠)
78		simprlr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡)
79		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑏𝑊𝑡)
80	4, 5	fpwwe2lem2 10043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
81	80	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
82	79, 81	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
83	82	simpld 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)))
84	83	simprd 499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
85	75, 77, 78, 84	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
86	85	ssbrd 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣 → 𝑤(𝑏 × 𝑏)𝑣))
87	74, 86	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
88		brxp 5565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑏))
89	88	simplbi 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤(𝑏 × 𝑏)𝑣 → 𝑤 ∈ 𝑏)
90	87, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑏)
91	90	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
92	61	elin2d 4126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑎)
93	92	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣 ∈ 𝑎)
94		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
95		brinxp2 5593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑎) ∧ 𝑤𝑡𝑣))
96	91, 93, 94, 95	syl21anbrc 1341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
97		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
98	97	breqd 5041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 ↔ 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
99	96, 98	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
100	75, 77, 20	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
101	100	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
102	101	ssbrd 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 → 𝑤(𝑎 × 𝑎)𝑣))
103	99, 102	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
104		brxp 5565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤 ∈ 𝑎 ∧ 𝑣 ∈ 𝑎))
105	104	simplbi 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤(𝑎 × 𝑎)𝑣 → 𝑤 ∈ 𝑎)
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
107	73, 106	elind 4121	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
108		breq1 5033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑤 → (𝑧𝑠𝑣 ↔ 𝑤𝑠𝑣))
109	108	rspcev 3571	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ (𝑛 ∩ 𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
110	107, 99, 109	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
111	72	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑛)
112		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎)
113	90	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏)
114	112, 113	sseldd 3916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
115	111, 114	elind 4121	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
116		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
117		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
118		inss1 4155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
119	117, 118	eqsstrdi 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
120	119	ssbrd 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣 → 𝑤𝑠𝑣))
121	116, 120	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
122	115, 121, 109	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
123	5	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝐴 ∈ V)
124		fpwwe2.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
125	124	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
127	4, 123, 125, 126, 79	fpwwe2lem10 10050	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
128	75, 77, 78, 127	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
129	110, 122, 128	mpjaodan 956	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
130	129	expr 460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
131	71, 130	syl5bir 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
132	131	expr 460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
133	132	exlimdv 1934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
134	70, 133	syl5bi 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
135	134	rexlimdv 3242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
136	68, 135	syl5bi 245	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑤∪ ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
137	65, 136	mtod 201	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ 𝑤∪ ran 𝑊 𝑣)
138	137	ralrimiva 3149	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
139	60, 62, 138	reximssdv 3235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
140	139	exp32 424	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
141	140	exlimdv 1934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
142	3, 141	syl5bi 245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
143	142	rexlimdv 3242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
144	45, 143	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
145	144	expr 460	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
146	145	exlimdv 1934	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (∃𝑦 𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
147	39, 146	syl5bi 245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑛 ≠ ∅ → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
148	147	expimpd 457	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
149	148	alrimiv 1928	. . . . . 6 ⊢ (𝜑 → ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
150		df-fr 5478	. . . . . 6 ⊢ (∪ ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
151	149, 150	sylibr 237	. . . . 5 ⊢ (𝜑 → ∪ ran 𝑊 Fr 𝑋)
152	1	eleq2i 2881	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑋 ↔ 𝑤 ∈ ∪ dom 𝑊)
153		eluni2 4804	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
154	152, 153	bitri 278	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
155	44, 154	anbi12i 629	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
156		reeanv 3320	. . . . . . . 8 ⊢ (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
157	155, 156	bitr4i 281	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ ∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏))
158		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
159	158	eldm 5733	. . . . . . . . . . 11 ⊢ (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
160	3, 159	anbi12i 629	. . . . . . . . . 10 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
161		exdistrv 1956	. . . . . . . . . 10 ⊢ (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
162	160, 161	bitr4i 281	. . . . . . . . 9 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ ∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡))
163	82	simprd 499	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
164	163	simpld 498	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 We 𝑏)
165	164	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
166		weso 5510	. . . . . . . . . . . . . . 15 ⊢ (𝑡 We 𝑏 → 𝑡 Or 𝑏)
167	165, 166	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
168		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎 ⊆ 𝑏)
169		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑎)
170	168, 169	sseldd 3916	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑏)
171		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
172		solin 5462	. . . . . . . . . . . . . 14 ⊢ ((𝑡 Or 𝑏 ∧ (𝑦 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏)) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
173	167, 170, 171, 172	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
174	21	relelrni 5783	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏𝑊𝑡 → 𝑡 ∈ ran 𝑊)
175	174	ad2antll 728	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
176	175	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
177		elssuni 4830	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ran 𝑊 → 𝑡 ⊆ ∪ ran 𝑊)
178	176, 177	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ ∪ ran 𝑊)
179	178	ssbrd 5073	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 → 𝑦∪ ran 𝑊 𝑤))
180		idd 24	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
181	178	ssbrd 5073	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦 → 𝑤∪ ran 𝑊 𝑦))
182	179, 180, 181	3orim123d 1441	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
183	173, 182	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
184	49	adantrr 716	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 We 𝑎)
185	184	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
186		weso 5510	. . . . . . . . . . . . . . 15 ⊢ (𝑠 We 𝑎 → 𝑠 Or 𝑎)
187	185, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
188		simplrl 776	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦 ∈ 𝑎)
189		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎)
190		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏)
191	189, 190	sseldd 3916	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
192		solin 5462	. . . . . . . . . . . . . 14 ⊢ ((𝑠 Or 𝑎 ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
193	187, 188, 191, 192	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
194	21	relelrni 5783	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑊𝑠 → 𝑠 ∈ ran 𝑊)
195	194	ad2antrl 727	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
196	195	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
197		elssuni 4830	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ran 𝑊 → 𝑠 ⊆ ∪ ran 𝑊)
198	196, 197	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ⊆ ∪ ran 𝑊)
199	198	ssbrd 5073	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 → 𝑦∪ ran 𝑊 𝑤))
200		idd 24	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
201	198	ssbrd 5073	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦 → 𝑤∪ ran 𝑊 𝑦))
202	199, 200, 201	3orim123d 1441	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
203	193, 202	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
204	127	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
205	183, 203, 204	mpjaodan 956	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
206	205	exp31 423	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
207	206	exlimdvv 1935	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
208	162, 207	syl5bi 245	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
209	208	rexlimdvv 3252	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
210	157, 209	syl5bi 245	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
211	210	ralrimivv 3155	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
212		dfwe2 7476	. . . . 5 ⊢ (∪ ran 𝑊 We 𝑋 ↔ (∪ ran 𝑊 Fr 𝑋 ∧ ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
213	151, 211, 212	sylanbrc 586	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 We 𝑋)
214	4	fpwwe2cbv 10041	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤 ∈ 𝑧 [(◡𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
215	5	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝐴 ∈ V)
216		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎𝑊𝑠)
217	214, 215, 216	fpwwe2lem3 10044	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎𝑊𝑠) ∧ 𝑦 ∈ 𝑎) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
218	217	anasss 470	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
219		cnvimass 5916	. . . . . . . . . . . . 13 ⊢ (◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊
220	5, 17	ssexd 5192	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ V)
221	220, 220	xpexd 7454	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 × 𝑋) ∈ V)
222	221, 37	ssexd 5192	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ ran 𝑊 ∈ V)
223	222	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∪ ran 𝑊 ∈ V)
224	223	dmexd 7596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → dom ∪ ran 𝑊 ∈ V)
225		ssexg 5191	. . . . . . . . . . . . 13 ⊢ (((◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊 ∧ dom ∪ ran 𝑊 ∈ V) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
226	219, 224, 225	sylancr 590	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
227		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (◡∪ ran 𝑊 “ {𝑦}) → 𝑢 = (◡∪ ran 𝑊 “ {𝑦}))
228		olc 865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
229		df-br 5031	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊)
230		eluni2 4804	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
231	229, 230	bitri 278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
232		df-br 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
233	84	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
234	233	ssbrd 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑏)𝑤))
235		brxp 5565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏))
236	235	simplbi 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑧(𝑏 × 𝑏)𝑤 → 𝑧 ∈ 𝑏)
237	234, 236	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧 ∈ 𝑏))
238	20	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
239	238	ssbrd 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑤𝑠𝑦 → 𝑤(𝑎 × 𝑎)𝑦))
240	239	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
241		brxp 5565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎))
242	241	simplbi 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤(𝑎 × 𝑎)𝑦 → 𝑤 ∈ 𝑎)
243	240, 242	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤 ∈ 𝑎)
244	243	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
245		elequ1 2118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎))
246	245	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑤 = 𝑦 → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
247	246	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
248	244, 247	jaodan 955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
249	248	impr 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → 𝑤 ∈ 𝑎)
250	249	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
251	237, 250	jctird 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎)))
252		brxp 5565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎))
253	251, 252	syl6ibr 255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑎)𝑤))
254	253	ancld 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
255		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
256	255	breqd 5041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ 𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
257		brin 5082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤))
258	256, 257	syl6bb 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
259	254, 258	sylibrd 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
260		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
261	260, 118	eqsstrdi 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
262	261	ssbrd 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
263	127	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
264	259, 262, 263	mpjaodan 956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
265	232, 264	syl5bir 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
266	265	exp32 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
267	266	expr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
268	267	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑦 ∈ 𝑎 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
269	268	impr 458	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
270	269	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
271	270	exlimdv 1934	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
272	70, 271	syl5bi 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
273	272	rexlimdv 3242	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
274	231, 273	syl5bi 245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
275	228, 274	sylan2 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤 = 𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
276	275	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
277	276	alrimiv 1928	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
278		breq2 5034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧∪ ran 𝑊 𝑦))
279		breq2 5034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧𝑠𝑤 ↔ 𝑧𝑠𝑦))
280	278, 279	imbi12d 348	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑦 → ((𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦)))
281	280	equsalvw 2010	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
282	277, 281	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
283	194	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ∈ ran 𝑊)
284	283, 197	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ⊆ ∪ ran 𝑊)
285	284	ssbrd 5073	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑠𝑦 → 𝑧∪ ran 𝑊 𝑦))
286	282, 285	impbid 215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 ↔ 𝑧𝑠𝑦))
287		vex 3444	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ V
288	287	eliniseg 5925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦))
289	288	elv 3446	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦)
290	287	eliniseg 5925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
291	290	elv 3446	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
292	286, 289, 291	3bitr4g 317	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (◡𝑠 “ {𝑦})))
293	292	eqrdv 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) = (◡𝑠 “ {𝑦}))
294	227, 293	sylan9eqr 2855	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → 𝑢 = (◡𝑠 “ {𝑦}))
295	294	sqxpeqd 5551	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
296	295	ineq2d 4139	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
297		relinxp 5651	. . . . . . . . . . . . . . . . 17 ⊢ Rel (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
298		relinxp 5651	. . . . . . . . . . . . . . . . 17 ⊢ Rel (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
299		vex 3444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
300	299	eliniseg 5925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ V → (𝑤 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
301	290, 300	anbi12d 633	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ V → ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)))
302	301	elv 3446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦))
303		orc 864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤𝑠𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
304	303, 274	sylan2 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
305	304	adantrl 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
306	284	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → 𝑠 ⊆ ∪ ran 𝑊)
307	306	ssbrd 5073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧𝑠𝑤 → 𝑧∪ ran 𝑊 𝑤))
308	305, 307	impbid 215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
309	302, 308	sylan2b 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦}))) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
310	309	pm5.32da 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
311		df-br 5031	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
312		brinxp2 5593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
313	311, 312	bitr3i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
314		df-br 5031	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
315		brinxp2 5593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
316	314, 315	bitr3i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
317	310, 313, 316	3bitr4g 317	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
318	297, 298, 317	eqrelrdv 5629	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
319	318	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
320	296, 319	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
321	294, 320	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
322	321	eqeq1d 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → ((𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
323	226, 322	sbcied 3762	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ([(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
324	218, 323	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
325	324	exp32 424	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
326	325	exlimdv 1934	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
327	3, 326	syl5bi 245	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
328	327	rexlimdv 3242	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
329	44, 328	syl5bi 245	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝑋 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
330	329	ralrimiv 3148	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
331	213, 330	jca 515	. . 3 ⊢ (𝜑 → (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
332	4, 5	fpwwe2lem2 10043	. . 3 ⊢ (𝜑 → (𝑋𝑊∪ ran 𝑊 ↔ ((𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
333	38, 331, 332	mpbir2and 712	. 2 ⊢ (𝜑 → 𝑋𝑊∪ ran 𝑊)
334	21	releldmi 5782	. 2 ⊢ (𝑋𝑊∪ ran 𝑊 → 𝑋 ∈ dom 𝑊)
335	333, 334	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∨ w3o 1083   ∧ w3a 1084  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441  [wsbc 3720   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ⟨cop 4531  ∪ cuni 4800   class class class wbr 5030  {copab 5092   Or wor 5437   Fr wfr 5475   We wwe 5477   × cxp 5517  ^◡ccnv 5518  dom cdm 5519  ran crn 5520   “ cima 5522  (class class class)co 7135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-wrecs 7930  df-recs 7991  df-oi 8958

This theorem is referenced by:  fpwwe2lem13  10053  fpwwe2  10054