Theorem fpwwe2lem11 10397

Description: Lemma for fpwwe2 10399. (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 3436	. . . . . . . . 9 ⊢ 𝑎 ∈ V
3	2	eldm 5809	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5		fpwwe2.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
6	4, 5	fpwwe2lem2 10388	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
7	6	simprbda 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)))
8	7	simpld 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝐴)
9		velpw 4538	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝒫 𝐴 ↔ 𝑎 ⊆ 𝐴)
10	8, 9	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
11	10	ex 413	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
12	11	exlimdv 1936	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
13	3, 12	syl5bi 241	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → 𝑎 ∈ 𝒫 𝐴))
14	13	ssrdv 3927	. . . . . 6 ⊢ (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15		sspwuni 5029	. . . . . 6 ⊢ (dom 𝑊 ⊆ 𝒫 𝐴 ↔ ∪ dom 𝑊 ⊆ 𝐴)
16	14, 15	sylib 217	. . . . 5 ⊢ (𝜑 → ∪ dom 𝑊 ⊆ 𝐴)
17	1, 16	eqsstrid 3969	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
18		vex 3436	. . . . . . . 8 ⊢ 𝑠 ∈ V
19	18	elrn 5802	. . . . . . 7 ⊢ (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
20	7	simprd 496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
21	4	relopabiv 5730	. . . . . . . . . . . . . . . 16 ⊢ Rel 𝑊
22	21	releldmi 5857	. . . . . . . . . . . . . . 15 ⊢ (𝑎𝑊𝑠 → 𝑎 ∈ dom 𝑊)
23	22	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24		elssuni 4871	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑊 → 𝑎 ⊆ ∪ dom 𝑊)
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ ∪ dom 𝑊)
26	25, 1	sseqtrrdi 3972	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝑋)
27		xpss12 5604	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
28	26, 26, 27	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
29	20, 28	sstrd 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30		velpw 4538	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
31	29, 30	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
32	31	ex 413	. . . . . . . 8 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
33	32	exlimdv 1936	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
34	19, 33	syl5bi 241	. . . . . 6 ⊢ (𝜑 → (𝑠 ∈ ran 𝑊 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
35	34	ssrdv 3927	. . . . 5 ⊢ (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36		sspwuni 5029	. . . . 5 ⊢ (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
37	35, 36	sylib 217	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
38	17, 37	jca 512	. . 3 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)))
39		n0 4280	. . . . . . . . 9 ⊢ (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑛)
40		ssel2 3916	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛) → 𝑦 ∈ 𝑋)
41	40	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → 𝑦 ∈ 𝑋)
42	1	eleq2i 2830	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ dom 𝑊)
43		eluni2 4843	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∪ dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
44	42, 43	bitri 274	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
45	41, 44	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
46	2	inex2 5242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ∈ V
47	46	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ∈ V)
48	6	simplbda 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
49	48	simpld 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 We 𝑎)
50	49	ad2ant2r 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 We 𝑎)
51		wefr 5579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 We 𝑎 → 𝑠 Fr 𝑎)
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 Fr 𝑎)
53		inss2 4163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ⊆ 𝑎
54	53	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ⊆ 𝑎)
55		simplrr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑛)
56		simprr 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑎)
57		inelcm 4398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑛 ∧ 𝑦 ∈ 𝑎) → (𝑛 ∩ 𝑎) ≠ ∅)
58	55, 56, 57	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ≠ ∅)
59		fri 5549	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∩ 𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛 ∩ 𝑎) ⊆ 𝑎 ∧ (𝑛 ∩ 𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
60	47, 52, 54, 58, 59	syl22anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
61		simprl 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛 ∩ 𝑎))
62	61	elin1d 4132	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑛)
63		simplrr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
64		ralnex 3167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
65	63, 64	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
66		df-br 5075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊)
67		eluni2 4843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
68	66, 67	bitri 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
69		vex 3436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑡 ∈ V
70	69	elrn 5802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
71		df-br 5075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
72		simprll 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑛)
73	72	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑛)
74		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣)
75		simp-4l 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑)
76		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑎𝑊𝑠)
77	76	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠)
78		simprlr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡)
79		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑏𝑊𝑡)
80	4, 5	fpwwe2lem2 10388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
81	80	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
82	79, 81	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
83	82	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)))
84	83	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
85	75, 77, 78, 84	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
86	85	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣 → 𝑤(𝑏 × 𝑏)𝑣))
87	74, 86	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
88		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑏))
89	88	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤(𝑏 × 𝑏)𝑣 → 𝑤 ∈ 𝑏)
90	87, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑏)
91	90	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
92	61	elin2d 4133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑎)
93	92	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣 ∈ 𝑎)
94		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
95		brinxp2 5664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑎) ∧ 𝑤𝑡𝑣))
96	91, 93, 94, 95	syl21anbrc 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
97		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
98	97	breqd 5085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 ↔ 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
99	96, 98	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
100	75, 77, 20	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
101	100	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
102	101	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 → 𝑤(𝑎 × 𝑎)𝑣))
103	99, 102	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
104		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤 ∈ 𝑎 ∧ 𝑣 ∈ 𝑎))
105	104	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤(𝑎 × 𝑎)𝑣 → 𝑤 ∈ 𝑎)
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
107	73, 106	elind 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
108		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑤 → (𝑧𝑠𝑣 ↔ 𝑤𝑠𝑣))
109	108	rspcev 3561	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ (𝑛 ∩ 𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
110	107, 99, 109	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
111	72	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑛)
112		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎)
113	90	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏)
114	112, 113	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
115	111, 114	elind 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
116		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
117		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
118		inss1 4162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
119	117, 118	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
120	119	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣 → 𝑤𝑠𝑣))
121	116, 120	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
122	115, 121, 109	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
123	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝐴 ∈ 𝑉)
124		fpwwe2.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
125	124	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
127	4, 123, 125, 126, 79	fpwwe2lem9 10395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
128	75, 77, 78, 127	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
129	110, 122, 128	mpjaodan 956	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
130	129	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
131	71, 130	syl5bir 242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
132	131	expr 457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
133	132	exlimdv 1936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
134	70, 133	syl5bi 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
135	134	rexlimdv 3212	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
136	68, 135	syl5bi 241	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑤∪ ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
137	65, 136	mtod 197	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ 𝑤∪ ran 𝑊 𝑣)
138	137	ralrimiva 3103	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
139	60, 62, 138	reximssdv 3205	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
140	139	exp32 421	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
141	140	exlimdv 1936	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
142	3, 141	syl5bi 241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
143	142	rexlimdv 3212	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
144	45, 143	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
145	144	expr 457	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
146	145	exlimdv 1936	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (∃𝑦 𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
147	39, 146	syl5bi 241	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑛 ≠ ∅ → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
148	147	expimpd 454	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
149	148	alrimiv 1930	. . . . . 6 ⊢ (𝜑 → ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
150		df-fr 5544	. . . . . 6 ⊢ (∪ ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
151	149, 150	sylibr 233	. . . . 5 ⊢ (𝜑 → ∪ ran 𝑊 Fr 𝑋)
152	1	eleq2i 2830	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑋 ↔ 𝑤 ∈ ∪ dom 𝑊)
153		eluni2 4843	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
154	152, 153	bitri 274	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
155	44, 154	anbi12i 627	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
156		reeanv 3294	. . . . . . . 8 ⊢ (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
157	155, 156	bitr4i 277	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ ∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏))
158		vex 3436	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
159	158	eldm 5809	. . . . . . . . . . 11 ⊢ (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
160	3, 159	anbi12i 627	. . . . . . . . . 10 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
161		exdistrv 1959	. . . . . . . . . 10 ⊢ (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
162	160, 161	bitr4i 277	. . . . . . . . 9 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ ∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡))
163	82	simprd 496	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
164	163	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 We 𝑏)
165	164	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
166		weso 5580	. . . . . . . . . . . . . . 15 ⊢ (𝑡 We 𝑏 → 𝑡 Or 𝑏)
167	165, 166	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
168		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎 ⊆ 𝑏)
169		simplrl 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑎)
170	168, 169	sseldd 3922	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑏)
171		simplrr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
172		solin 5528	. . . . . . . . . . . . . 14 ⊢ ((𝑡 Or 𝑏 ∧ (𝑦 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏)) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
173	167, 170, 171, 172	syl12anc 834	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
174	21	relelrni 5858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏𝑊𝑡 → 𝑡 ∈ ran 𝑊)
175	174	ad2antll 726	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
176	175	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
177		elssuni 4871	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ran 𝑊 → 𝑡 ⊆ ∪ ran 𝑊)
178	176, 177	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ ∪ ran 𝑊)
179	178	ssbrd 5117	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 → 𝑦∪ ran 𝑊 𝑤))
180		idd 24	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
181	178	ssbrd 5117	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦 → 𝑤∪ ran 𝑊 𝑦))
182	179, 180, 181	3orim123d 1443	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
183	173, 182	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
184	49	adantrr 714	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 We 𝑎)
185	184	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
186		weso 5580	. . . . . . . . . . . . . . 15 ⊢ (𝑠 We 𝑎 → 𝑠 Or 𝑎)
187	185, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
188		simplrl 774	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦 ∈ 𝑎)
189		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎)
190		simplrr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏)
191	189, 190	sseldd 3922	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
192		solin 5528	. . . . . . . . . . . . . 14 ⊢ ((𝑠 Or 𝑎 ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
193	187, 188, 191, 192	syl12anc 834	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
194	21	relelrni 5858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑊𝑠 → 𝑠 ∈ ran 𝑊)
195	194	ad2antrl 725	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
196	195	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
197		elssuni 4871	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ran 𝑊 → 𝑠 ⊆ ∪ ran 𝑊)
198	196, 197	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ⊆ ∪ ran 𝑊)
199	198	ssbrd 5117	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 → 𝑦∪ ran 𝑊 𝑤))
200		idd 24	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
201	198	ssbrd 5117	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦 → 𝑤∪ ran 𝑊 𝑦))
202	199, 200, 201	3orim123d 1443	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
203	193, 202	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
204	127	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
205	183, 203, 204	mpjaodan 956	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
206	205	exp31 420	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
207	206	exlimdvv 1937	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
208	162, 207	syl5bi 241	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
209	208	rexlimdvv 3222	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
210	157, 209	syl5bi 241	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
211	210	ralrimivv 3122	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
212		dfwe2 7624	. . . . 5 ⊢ (∪ ran 𝑊 We 𝑋 ↔ (∪ ran 𝑊 Fr 𝑋 ∧ ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
213	151, 211, 212	sylanbrc 583	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 We 𝑋)
214	4	fpwwe2cbv 10386	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤 ∈ 𝑧 [(◡𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
215	5	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝐴 ∈ 𝑉)
216		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎𝑊𝑠)
217	214, 215, 216	fpwwe2lem3 10389	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎𝑊𝑠) ∧ 𝑦 ∈ 𝑎) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
218	217	anasss 467	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
219		cnvimass 5989	. . . . . . . . . . . . 13 ⊢ (◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊
220	5, 17	ssexd 5248	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ V)
221	220, 220	xpexd 7601	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 × 𝑋) ∈ V)
222	221, 37	ssexd 5248	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ ran 𝑊 ∈ V)
223	222	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∪ ran 𝑊 ∈ V)
224	223	dmexd 7752	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → dom ∪ ran 𝑊 ∈ V)
225		ssexg 5247	. . . . . . . . . . . . 13 ⊢ (((◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊 ∧ dom ∪ ran 𝑊 ∈ V) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
226	219, 224, 225	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
227		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (◡∪ ran 𝑊 “ {𝑦}) → 𝑢 = (◡∪ ran 𝑊 “ {𝑦}))
228		olc 865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
229		df-br 5075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊)
230		eluni2 4843	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
231	229, 230	bitri 274	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
232		df-br 5075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
233	84	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
234	233	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑏)𝑤))
235		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏))
236	235	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑧(𝑏 × 𝑏)𝑤 → 𝑧 ∈ 𝑏)
237	234, 236	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧 ∈ 𝑏))
238	20	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
239	238	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑤𝑠𝑦 → 𝑤(𝑎 × 𝑎)𝑦))
240	239	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
241		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎))
242	241	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤(𝑎 × 𝑎)𝑦 → 𝑤 ∈ 𝑎)
243	240, 242	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤 ∈ 𝑎)
244	243	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
245		elequ1 2113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎))
246	245	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑤 = 𝑦 → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
247	246	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
248	244, 247	jaodan 955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
249	248	impr 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → 𝑤 ∈ 𝑎)
250	249	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
251	237, 250	jctird 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎)))
252		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎))
253	251, 252	syl6ibr 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑎)𝑤))
254	253	ancld 551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
255		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
256	255	breqd 5085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ 𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
257		brin 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤))
258	256, 257	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
259	254, 258	sylibrd 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
260		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
261	260, 118	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
262	261	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
263	127	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
264	259, 262, 263	mpjaodan 956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
265	232, 264	syl5bir 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
266	265	exp32 421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
267	266	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
268	267	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑦 ∈ 𝑎 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
269	268	impr 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
270	269	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
271	270	exlimdv 1936	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
272	70, 271	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
273	272	rexlimdv 3212	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
274	231, 273	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
275	228, 274	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤 = 𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
276	275	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
277	276	alrimiv 1930	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
278		breq2 5078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧∪ ran 𝑊 𝑦))
279		breq2 5078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧𝑠𝑤 ↔ 𝑧𝑠𝑦))
280	278, 279	imbi12d 345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑦 → ((𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦)))
281	280	equsalvw 2007	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
282	277, 281	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
283	194	ad2antrl 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ∈ ran 𝑊)
284	283, 197	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ⊆ ∪ ran 𝑊)
285	284	ssbrd 5117	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑠𝑦 → 𝑧∪ ran 𝑊 𝑦))
286	282, 285	impbid 211	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 ↔ 𝑧𝑠𝑦))
287		vex 3436	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ V
288	287	eliniseg 6002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦))
289	288	elv 3438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦)
290	287	eliniseg 6002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
291	290	elv 3438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
292	286, 289, 291	3bitr4g 314	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (◡𝑠 “ {𝑦})))
293	292	eqrdv 2736	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) = (◡𝑠 “ {𝑦}))
294	227, 293	sylan9eqr 2800	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → 𝑢 = (◡𝑠 “ {𝑦}))
295	294	sqxpeqd 5621	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
296	295	ineq2d 4146	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
297		relinxp 5724	. . . . . . . . . . . . . . . . 17 ⊢ Rel (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
298		relinxp 5724	. . . . . . . . . . . . . . . . 17 ⊢ Rel (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
299		vex 3436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
300	299	eliniseg 6002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ V → (𝑤 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
301	290, 300	anbi12d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ V → ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)))
302	301	elv 3438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦))
303		orc 864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤𝑠𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
304	303, 274	sylan2 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
305	304	adantrl 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
306	284	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → 𝑠 ⊆ ∪ ran 𝑊)
307	306	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧𝑠𝑤 → 𝑧∪ ran 𝑊 𝑤))
308	305, 307	impbid 211	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
309	302, 308	sylan2b 594	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦}))) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
310	309	pm5.32da 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
311		df-br 5075	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
312		brinxp2 5664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
313	311, 312	bitr3i 276	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
314		df-br 5075	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
315		brinxp2 5664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
316	314, 315	bitr3i 276	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
317	310, 313, 316	3bitr4g 314	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
318	297, 298, 317	eqrelrdv 5702	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
319	318	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
320	296, 319	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
321	294, 320	oveq12d 7293	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
322	321	eqeq1d 2740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → ((𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
323	226, 322	sbcied 3761	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ([(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
324	218, 323	mpbird 256	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
325	324	exp32 421	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
326	325	exlimdv 1936	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
327	3, 326	syl5bi 241	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
328	327	rexlimdv 3212	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
329	44, 328	syl5bi 241	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝑋 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
330	329	ralrimiv 3102	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
331	213, 330	jca 512	. . 3 ⊢ (𝜑 → (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
332	4, 5	fpwwe2lem2 10388	. . 3 ⊢ (𝜑 → (𝑋𝑊∪ ran 𝑊 ↔ ((𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
333	38, 331, 332	mpbir2and 710	. 2 ⊢ (𝜑 → 𝑋𝑊∪ ran 𝑊)
334	21	releldmi 5857	. 2 ⊢ (𝑋𝑊∪ ran 𝑊 → 𝑋 ∈ dom 𝑊)
335	333, 334	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∨ w3o 1085   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432  [wsbc 3716   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561  ⟨cop 4567  ∪ cuni 4839   class class class wbr 5074  {copab 5136   Or wor 5502   Fr wfr 5541   We wwe 5543   × cxp 5587  ^◡ccnv 5588  dom cdm 5589  ran crn 5590   “ cima 5592  (class class class)co 7275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-oi 9269

This theorem is referenced by:  fpwwe2lem12  10398  fpwwe2  10399