Theorem fpwwe2lem11 10710

Description: Lemma for fpwwe2 10712. (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 3492	. . . . . . . . 9 ⊢ 𝑎 ∈ V
3	2	eldm 5925	. . . . . . . 8 ⊢ (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5		fpwwe2.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
6	4, 5	fpwwe2lem2 10701	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
7	6	simprbda 498	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)))
8	7	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝐴)
9		velpw 4627	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝒫 𝐴 ↔ 𝑎 ⊆ 𝐴)
10	8, 9	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
11	10	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
12	11	exlimdv 1932	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → 𝑎 ∈ 𝒫 𝐴))
13	3, 12	biimtrid 242	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → 𝑎 ∈ 𝒫 𝐴))
14	13	ssrdv 4014	. . . . . 6 ⊢ (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15		sspwuni 5123	. . . . . 6 ⊢ (dom 𝑊 ⊆ 𝒫 𝐴 ↔ ∪ dom 𝑊 ⊆ 𝐴)
16	14, 15	sylib 218	. . . . 5 ⊢ (𝜑 → ∪ dom 𝑊 ⊆ 𝐴)
17	1, 16	eqsstrid 4057	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
18		vex 3492	. . . . . . . 8 ⊢ 𝑠 ∈ V
19	18	elrn 5918	. . . . . . 7 ⊢ (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
20	7	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
21	4	relopabiv 5844	. . . . . . . . . . . . . . . 16 ⊢ Rel 𝑊
22	21	releldmi 5973	. . . . . . . . . . . . . . 15 ⊢ (𝑎𝑊𝑠 → 𝑎 ∈ dom 𝑊)
23	22	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24		elssuni 4961	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑊 → 𝑎 ⊆ ∪ dom 𝑊)
25	23, 24	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ ∪ dom 𝑊)
26	25, 1	sseqtrrdi 4060	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎 ⊆ 𝑋)
27		xpss12 5715	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
28	26, 26, 27	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
29	20, 28	sstrd 4019	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30		velpw 4627	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
31	29, 30	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
32	31	ex 412	. . . . . . . 8 ⊢ (𝜑 → (𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
33	32	exlimdv 1932	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 𝑎𝑊𝑠 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
34	19, 33	biimtrid 242	. . . . . 6 ⊢ (𝜑 → (𝑠 ∈ ran 𝑊 → 𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
35	34	ssrdv 4014	. . . . 5 ⊢ (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36		sspwuni 5123	. . . . 5 ⊢ (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
37	35, 36	sylib 218	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 ⊆ (𝑋 × 𝑋))
38	17, 37	jca 511	. . 3 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)))
39		n0 4376	. . . . . . . . 9 ⊢ (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑛)
40		ssel2 4003	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛) → 𝑦 ∈ 𝑋)
41	40	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → 𝑦 ∈ 𝑋)
42	1	eleq2i 2836	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ dom 𝑊)
43		eluni2 4935	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∪ dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
44	42, 43	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
45	41, 44	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎)
46	2	inex2 5336	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ∈ V
47	46	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ∈ V)
48	6	simplbda 499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦 ∈ 𝑎 [(◡𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
49	48	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑠 We 𝑎)
50	49	ad2ant2r 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 We 𝑎)
51		wefr 5690	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 We 𝑎 → 𝑠 Fr 𝑎)
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 Fr 𝑎)
53		inss2 4259	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∩ 𝑎) ⊆ 𝑎
54	53	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ⊆ 𝑎)
55		simplrr 777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑛)
56		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑦 ∈ 𝑎)
57		inelcm 4488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑛 ∧ 𝑦 ∈ 𝑎) → (𝑛 ∩ 𝑎) ≠ ∅)
58	55, 56, 57	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑛 ∩ 𝑎) ≠ ∅)
59		fri 5657	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 ∩ 𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛 ∩ 𝑎) ⊆ 𝑎 ∧ (𝑛 ∩ 𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
60	47, 52, 54, 58, 59	syl22anc 838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ (𝑛 ∩ 𝑎)∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
61		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛 ∩ 𝑎))
62	61	elin1d 4227	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑛)
63		simplrr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)
64		ralnex 3078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
65	63, 64	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
66		df-br 5167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊)
67		eluni2 4935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑤, 𝑣⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
68	66, 67	bitri 275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤∪ ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡)
69		vex 3492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑡 ∈ V
70	69	elrn 5918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
71		df-br 5167	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
72		simprll 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑛)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
81	80	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
82	79, 81	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
83	82	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑏 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑏 × 𝑏)))
84	83	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
85	75, 77, 78, 84	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
86	85	ssbrd 5209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣 → 𝑤(𝑏 × 𝑏)𝑣))
87	74, 86	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
88		brxp 5749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑏))
89	88	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑤(𝑏 × 𝑏)𝑣 → 𝑤 ∈ 𝑏)
90	87, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤 ∈ 𝑏)
91	90	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
92	61	elin2d 4228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ 𝑎)
93	92	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣 ∈ 𝑎)
94		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
95		brinxp2 5777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤 ∈ 𝑏 ∧ 𝑣 ∈ 𝑎) ∧ 𝑤𝑡𝑣))
96	91, 93, 94, 95	syl21anbrc 1344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
97		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
98	97	breqd 5177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 ↔ 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
99	96, 98	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
100	75, 77, 20	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
102	101	ssbrd 5209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣 → 𝑤(𝑎 × 𝑎)𝑣))
103	99, 102	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
104		brxp 5749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤 ∈ 𝑎 ∧ 𝑣 ∈ 𝑎))
105	104	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤(𝑎 × 𝑎)𝑣 → 𝑤 ∈ 𝑎)
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
107	73, 106	elind 4223	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
108		breq1 5169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑤 → (𝑧𝑠𝑣 ↔ 𝑤𝑠𝑣))
109	108	rspcev 3635	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑤 ∈ (𝑛 ∩ 𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
110	107, 99, 109	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
111	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑛)
112		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏 ⊆ 𝑎)
113	90	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑏)
114	112, 113	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
115	111, 114	elind 4223	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛 ∩ 𝑎))
116		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
117		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
118		inss1 4258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
119	117, 118	eqsstrdi 4063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
120	119	ssbrd 5209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣 → 𝑤𝑠𝑣))
121	116, 120	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
122	115, 121, 109	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
123	5	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝐴 ∈ 𝑉)
124		fpwwe2.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
125	124	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
127	4, 123, 125, 126, 79	fpwwe2lem9 10708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
128	75, 77, 78, 127	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
129	110, 122, 128	mpjaodan 959	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)
130	129	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
131	71, 130	biimtrrid 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤 ∈ 𝑛 ∧ 𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
132	131	expr 456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
133	132	exlimdv 1932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
134	70, 133	biimtrid 242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣)))
135	134	rexlimdv 3159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (∃𝑡 ∈ ran 𝑊⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
136	68, 135	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → (𝑤∪ ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛 ∩ 𝑎)𝑧𝑠𝑣))
137	65, 136	mtod 198	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤 ∈ 𝑛) → ¬ 𝑤∪ ran 𝑊 𝑣)
138	137	ralrimiva 3152	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑣 ∈ (𝑛 ∩ 𝑎) ∧ ∀𝑧 ∈ (𝑛 ∩ 𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
139	60, 62, 138	reximssdv 3179	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
140	139	exp32 420	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
141	140	exlimdv 1932	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
142	3, 141	biimtrid 242	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)))
143	142	rexlimdv 3159	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
144	45, 143	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛)) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣)
145	144	expr 456	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
146	145	exlimdv 1932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (∃𝑦 𝑦 ∈ 𝑛 → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
147	39, 146	biimtrid 242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ⊆ 𝑋) → (𝑛 ≠ ∅ → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
148	147	expimpd 453	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
149	148	alrimiv 1926	. . . . . 6 ⊢ (𝜑 → ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
150		df-fr 5652	. . . . . 6 ⊢ (∪ ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛 ⊆ 𝑋 ∧ 𝑛 ≠ ∅) → ∃𝑣 ∈ 𝑛 ∀𝑤 ∈ 𝑛 ¬ 𝑤∪ ran 𝑊 𝑣))
151	149, 150	sylibr 234	. . . . 5 ⊢ (𝜑 → ∪ ran 𝑊 Fr 𝑋)
152	1	eleq2i 2836	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑋 ↔ 𝑤 ∈ ∪ dom 𝑊)
153		eluni2 4935	. . . . . . . . . 10 ⊢ (𝑤 ∈ ∪ dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
154	152, 153	bitri 275	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏)
155	44, 154	anbi12i 627	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
156		reeanv 3235	. . . . . . . 8 ⊢ (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤 ∈ 𝑏))
157	155, 156	bitr4i 278	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ↔ ∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏))
158		vex 3492	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
159	158	eldm 5925	. . . . . . . . . . 11 ⊢ (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
160	3, 159	anbi12i 627	. . . . . . . . . 10 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
161		exdistrv 1955	. . . . . . . . . 10 ⊢ (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
162	160, 161	bitr4i 278	. . . . . . . . 9 ⊢ ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) ↔ ∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡))
163	82	simprd 495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦 ∈ 𝑏 [(◡𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
164	163	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 We 𝑏)
165	164	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
166		weso 5691	. . . . . . . . . . . . . . 15 ⊢ (𝑡 We 𝑏 → 𝑡 Or 𝑏)
167	165, 166	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
168		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎 ⊆ 𝑏)
169		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑎)
170	168, 169	sseldd 4009	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦 ∈ 𝑏)
171		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑏)
172		solin 5634	. . . . . . . . . . . . . 14 ⊢ ((𝑡 Or 𝑏 ∧ (𝑦 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏)) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
173	167, 170, 171, 172	syl12anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑡𝑦))
174	21	relelrni 5974	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏𝑊𝑡 → 𝑡 ∈ ran 𝑊)
175	174	ad2antll 728	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
176	175	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
177		elssuni 4961	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ran 𝑊 → 𝑡 ⊆ ∪ ran 𝑊)
178	176, 177	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ ∪ ran 𝑊)
179	178	ssbrd 5209	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤 → 𝑦∪ ran 𝑊 𝑤))
180		idd 24	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
181	178	ssbrd 5209	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦 → 𝑤∪ ran 𝑊 𝑦))
182	179, 180, 181	3orim123d 1444	. . . . . . . . . . . . 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 5691	. . . . . . . . . . . . . . 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 4009	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ 𝑎)
192		solin 5634	. . . . . . . . . . . . . 14 ⊢ ((𝑠 Or 𝑎 ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
193	187, 188, 191, 192	syl12anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦))
194	21	relelrni 5974	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑊𝑠 → 𝑠 ∈ ran 𝑊)
195	194	ad2antrl 727	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
196	195	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
197		elssuni 4961	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ran 𝑊 → 𝑠 ⊆ ∪ ran 𝑊)
198	196, 197	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ⊆ ∪ ran 𝑊)
199	198	ssbrd 5209	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤 → 𝑦∪ ran 𝑊 𝑤))
200		idd 24	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤 → 𝑦 = 𝑤))
201	198	ssbrd 5209	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦 → 𝑤∪ ran 𝑊 𝑦))
202	199, 200, 201	3orim123d 1444	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤𝑠𝑦) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
203	193, 202	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
204	127	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
205	183, 203, 204	mpjaodan 959	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏)) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
206	205	exp31 419	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
207	206	exlimdvv 1933	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑠∃𝑡(𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
208	162, 207	biimtrid 242	. . . . . . . 8 ⊢ (𝜑 → ((𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊) → ((𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))))
209	208	rexlimdvv 3218	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊∃𝑏 ∈ dom 𝑊(𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
210	157, 209	biimtrid 242	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
211	210	ralrimivv 3206	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦))
212		dfwe2 7809	. . . . 5 ⊢ (∪ ran 𝑊 We 𝑋 ↔ (∪ ran 𝑊 Fr 𝑋 ∧ ∀𝑦 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑦∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤∪ ran 𝑊 𝑦)))
213	151, 211, 212	sylanbrc 582	. . . 4 ⊢ (𝜑 → ∪ ran 𝑊 We 𝑋)
214	4	fpwwe2cbv 10699	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧 ⊆ 𝐴 ∧ 𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤 ∈ 𝑧 [(◡𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
215	5	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝐴 ∈ 𝑉)
216		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → 𝑎𝑊𝑠)
217	214, 215, 216	fpwwe2lem3 10702	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎𝑊𝑠) ∧ 𝑦 ∈ 𝑎) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
218	217	anasss 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦)
219		cnvimass 6111	. . . . . . . . . . . . 13 ⊢ (◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊
220	5, 17	ssexd 5342	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ V)
221	220, 220	xpexd 7786	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 × 𝑋) ∈ V)
222	221, 37	ssexd 5342	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ ran 𝑊 ∈ V)
223	222	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∪ ran 𝑊 ∈ V)
224	223	dmexd 7943	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → dom ∪ ran 𝑊 ∈ V)
225		ssexg 5341	. . . . . . . . . . . . 13 ⊢ (((◡∪ ran 𝑊 “ {𝑦}) ⊆ dom ∪ ran 𝑊 ∧ dom ∪ ran 𝑊 ∈ V) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
226	219, 224, 225	sylancr 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) ∈ V)
227		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (◡∪ ran 𝑊 “ {𝑦}) → 𝑢 = (◡∪ ran 𝑊 “ {𝑦}))
228		olc 867	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
229		df-br 5167	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊)
230		eluni2 4935	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑧, 𝑤⟩ ∈ ∪ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
231	229, 230	bitri 275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧∪ ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡)
232		df-br 5167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
233	84	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
234	233	ssbrd 5209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑏)𝑤))
235		brxp 5749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑏))
236	235	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑧(𝑏 × 𝑏)𝑤 → 𝑧 ∈ 𝑏)
237	234, 236	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧 ∈ 𝑏))
238	20	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
239	238	ssbrd 5209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → (𝑤𝑠𝑦 → 𝑤(𝑎 × 𝑎)𝑦))
240	239	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
241		brxp 5749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎))
242	241	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤(𝑎 × 𝑎)𝑦 → 𝑤 ∈ 𝑎)
243	240, 242	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤 ∈ 𝑎)
244	243	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
245		elequ1 2115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎))
246	245	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑤 = 𝑦 → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
247	246	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
248	244, 247	jaodan 958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑦 ∈ 𝑎 → 𝑤 ∈ 𝑎))
249	248	impr 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → 𝑤 ∈ 𝑎)
250	249	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ 𝑎)
251	237, 250	jctird 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎)))
252		brxp 5749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧 ∈ 𝑏 ∧ 𝑤 ∈ 𝑎))
253	251, 252	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧(𝑏 × 𝑎)𝑤))
254	253	ancld 550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
255		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
256	255	breqd 5177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ 𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
257		brin 5218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤))
258	256, 257	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤 ∧ 𝑧(𝑏 × 𝑎)𝑤)))
259	254, 258	sylibrd 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
260		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
261	260, 118	eqsstrdi 4063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 ⊆ 𝑠)
262	261	ssbrd 5209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) ∧ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
263	127	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → ((𝑎 ⊆ 𝑏 ∧ 𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏 ⊆ 𝑎 ∧ 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
264	259, 262, 263	mpjaodan 959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑡𝑤 → 𝑧𝑠𝑤))
265	232, 264	biimtrrid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
266	265	exp32 420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑏𝑊𝑡)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
267	266	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑦 ∈ 𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
268	267	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑎𝑊𝑠) → (𝑦 ∈ 𝑎 → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))))
269	268	impr 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ((𝑤𝑠𝑦 ∨ 𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))))
270	269	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
271	270	exlimdv 1932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
272	70, 271	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤)))
273	272	rexlimdv 3159	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊⟨𝑧, 𝑤⟩ ∈ 𝑡 → 𝑧𝑠𝑤))
274	231, 273	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
275	228, 274	sylan2 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤 = 𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
276	275	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
277	276	alrimiv 1926	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)))
278		breq2 5170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧∪ ran 𝑊 𝑦))
279		breq2 5170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑦 → (𝑧𝑠𝑤 ↔ 𝑧𝑠𝑦))
280	278, 279	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑦 → ((𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦)))
281	280	equsalvw 2003	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤(𝑤 = 𝑦 → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤)) ↔ (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
282	277, 281	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 → 𝑧𝑠𝑦))
283	194	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ∈ ran 𝑊)
284	283, 197	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → 𝑠 ⊆ ∪ ran 𝑊)
285	284	ssbrd 5209	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧𝑠𝑦 → 𝑧∪ ran 𝑊 𝑦))
286	282, 285	impbid 212	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧∪ ran 𝑊 𝑦 ↔ 𝑧𝑠𝑦))
287		vex 3492	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ V
288	287	eliniseg 6124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦))
289	288	elv 3493	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧∪ ran 𝑊 𝑦)
290	287	eliniseg 6124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ V → (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
291	290	elv 3493	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
292	286, 289, 291	3bitr4g 314	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (𝑧 ∈ (◡∪ ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (◡𝑠 “ {𝑦})))
293	292	eqrdv 2738	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (◡∪ ran 𝑊 “ {𝑦}) = (◡𝑠 “ {𝑦}))
294	227, 293	sylan9eqr 2802	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → 𝑢 = (◡𝑠 “ {𝑦}))
295	294	sqxpeqd 5732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
296	295	ineq2d 4241	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
297		relinxp 5838	. . . . . . . . . . . . . . . . 17 ⊢ Rel (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
298		relinxp 5838	. . . . . . . . . . . . . . . . 17 ⊢ Rel (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))
299		vex 3492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
300	299	eliniseg 6124	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ V → (𝑤 ∈ (◡𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
301	290, 300	anbi12d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ V → ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)))
302	301	elv 3493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦))
303		orc 866	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤𝑠𝑦 → (𝑤𝑠𝑦 ∨ 𝑤 = 𝑦))
304	303, 274	sylan2 592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
305	304	adantrl 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 → 𝑧𝑠𝑤))
306	284	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → 𝑠 ⊆ ∪ ran 𝑊)
307	306	ssbrd 5209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧𝑠𝑤 → 𝑧∪ ran 𝑊 𝑤))
308	305, 307	impbid 212	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧𝑠𝑦 ∧ 𝑤𝑠𝑦)) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
309	302, 308	sylan2b 593	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ (𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦}))) → (𝑧∪ ran 𝑊 𝑤 ↔ 𝑧𝑠𝑤))
310	309	pm5.32da 578	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
311		df-br 5167	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
312		brinxp2 5777	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
313	311, 312	bitr3i 277	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧∪ ran 𝑊 𝑤))
314		df-br 5167	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
315		brinxp2 5777	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
316	314, 315	bitr3i 277	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (◡𝑠 “ {𝑦}) ∧ 𝑤 ∈ (◡𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
317	310, 313, 316	3bitr4g 314	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (⟨𝑧, 𝑤⟩ ∈ (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
318	297, 298, 317	eqrelrdv 5816	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
319	318	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
320	296, 319	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (∪ ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦}))))
321	294, 320	oveq12d 7466	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → (𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))))
322	321	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) ∧ 𝑢 = (◡∪ ran 𝑊 “ {𝑦})) → ((𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
323	226, 322	sbcied 3850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → ([(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((◡𝑠 “ {𝑦})𝐹(𝑠 ∩ ((◡𝑠 “ {𝑦}) × (◡𝑠 “ {𝑦})))) = 𝑦))
324	218, 323	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎𝑊𝑠 ∧ 𝑦 ∈ 𝑎)) → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
325	324	exp32 420	. . . . . . . . 9 ⊢ (𝜑 → (𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
326	325	exlimdv 1932	. . . . . . . 8 ⊢ (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
327	3, 326	biimtrid 242	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
328	327	rexlimdv 3159	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
329	44, 328	biimtrid 242	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝑋 → [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
330	329	ralrimiv 3151	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
331	213, 330	jca 511	. . 3 ⊢ (𝜑 → (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
332	4, 5	fpwwe2lem2 10701	. . 3 ⊢ (𝜑 → (𝑋𝑊∪ ran 𝑊 ↔ ((𝑋 ⊆ 𝐴 ∧ ∪ ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ (∪ ran 𝑊 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡∪ ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹(∪ ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
333	38, 331, 332	mpbir2and 712	. 2 ⊢ (𝜑 → 𝑋𝑊∪ ran 𝑊)
334	21	releldmi 5973	. 2 ⊢ (𝑋𝑊∪ ran 𝑊 → 𝑋 ∈ dom 𝑊)
335	333, 334	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∨ w3o 1086   ∧ w3a 1087  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  Vcvv 3488  [wsbc 3804   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  𝒫 cpw 4622  {csn 4648  ⟨cop 4654  ∪ cuni 4931   class class class wbr 5166  {copab 5228   Or wor 5606   Fr wfr 5649   We wwe 5651   × cxp 5698  ^◡ccnv 5699  dom cdm 5700  ran crn 5701   “ cima 5703  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-oi 9579

This theorem is referenced by:  fpwwe2lem12  10711  fpwwe2  10712