fpwwe2lem12 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fpwwe2lem12		Structured version Visualization version GIF version

Theorem fpwwe2lem12 10329

Description: Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)

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

**Assertion**
Ref	Expression
fpwwe2lem12	⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)

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		ssun2 4103	. . . 4 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
2		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3		fpwwe2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝐴 ∈ 𝑉)
5		fpwwe2.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
6	5	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7		fpwwe2.4	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ dom 𝑊
8	2, 4, 6, 7	fpwwe2lem11 10328	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
9	2, 4, 6, 7	fpwwe2lem10 10327	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10		ffun 6587	. . . . . . . . . . . . . 14 ⊢ (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11		funfvbrb 6910	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
12	9, 10, 11	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
13	8, 12	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊‘𝑋))
14	2, 4	fpwwe2lem2 10319	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊‘𝑋) ↔ ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
15	13, 14	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
16	15	simpld 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)))
17	16	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ⊆ 𝐴)
18	16	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
19	15	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
20	19	simpld 494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) We 𝑋)
21	17, 18, 20	3jca 1126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋))
22	2, 3, 5	fpwwe2lem4 10321	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
23	21, 22	syldan 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
24	23	snssd 4739	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝐴)
25	17, 24	unssd 4116	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴)
26		ssun1 4102	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
27		xpss12 5595	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
28	26, 26, 27	mp2an 688	. . . . . . . . . 10 ⊢ (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
29	18, 28	sstrdi 3929	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
30		xpss12 5595	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
31	26, 1, 30	mp2an 688	. . . . . . . . . 10 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
32	31	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
33	29, 32	unssd 4116	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
34	25, 33	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))))
35		ssdif0 4294	. . . . . . . . . . . . . 14 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
36		simpllr 772	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
37	18	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
38	37	ssbrd 5113	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋))))
39		brxp 5627	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
40	39	simplbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
41	38, 40	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
42	36, 41	mtod 197	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)))
43		brxp 5627	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ {(𝑋𝐹(𝑊‘𝑋))}))
44	43	simplbi 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
45	36, 44	nsyl 140	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))
46		ovex 7288	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐹(𝑊‘𝑋)) ∈ V
47		breq2 5074	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋))))
48		brun 5121	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
49	47, 48	bitrdi 286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
50	49	notbid 317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → (¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
51	46, 50	rexsn 4615	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
52		ioran 980	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
53	51, 52	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
54	42, 45, 53	sylanbrc 582	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
55		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))})
56		sssn 4756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
57	55, 56	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
58		simplrr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ≠ ∅)
59	58	neneqd 2947	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑥 = ∅)
60	57, 59	orcnd 875	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊‘𝑋))})
61	60	raleqdv 3339	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
62		breq1 5073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
63	62	notbid 317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
64	46, 63	ralsn 4614	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
65	61, 64	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
66	60, 65	rexeqbidv 3328	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
67	54, 66	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
68	67	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
69	35, 68	syl5bir 242	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
70		vex 3426	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
71		difexg 5246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
72	70, 71	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
73		wefr 5570	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
74	20, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Fr 𝑋)
75	74	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑊‘𝑋) Fr 𝑋)
76		simplrl 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
77		uncom 4083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋)
78	76, 77	sseqtrdi 3967	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋))
79		ssundif 4415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
80	78, 79	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
81		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)
82		fri 5540	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
83	72, 75, 80, 81, 82	syl22anc 835	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
84		brun 5121	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
85		idd 24	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑊‘𝑋)𝑦 → 𝑧(𝑊‘𝑋)𝑦))
86		brxp 5627	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑧 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
87	86	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
88		eldifn 4058	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
89	88	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
90	89	pm2.21d 121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑧(𝑊‘𝑋)𝑦))
91	87, 90	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑧(𝑊‘𝑋)𝑦))
92	85, 91	jaod 855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) → 𝑧(𝑊‘𝑋)𝑦))
93	84, 92	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → 𝑧(𝑊‘𝑋)𝑦))
94	93	con3d 152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (¬ 𝑧(𝑊‘𝑋)𝑦 → ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
95	94	ralimdv 3103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
96		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
97	96	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
98	18	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
99	98	ssbrd 5113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦))
100		brxp 5627	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))
101	100	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
102	99, 101	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
103	97, 102	mtod 197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦)
104		brxp 5627	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
105	104	simprbi 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
106	89, 105	nsyl 140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
107		brun 5121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
108	62, 107	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
109	108	notbid 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
110	46, 109	ralsn 4614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
111		ioran 980	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
112	110, 111	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
113	103, 106, 112	sylanbrc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
114	95, 113	jctird 526	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
115		ssun1 4102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
116		undif1 4406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
117	115, 116	sseqtrri 3954	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))})
118		ralun 4122	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
119		ssralv 3983	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
120	117, 118, 119	mpsyl 68	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
121	114, 120	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
122		eldifi 4057	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 ∈ 𝑥)
123	122	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑦 ∈ 𝑥)
124	121, 123	jctild 525	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
125	124	expimpd 453	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦) → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
126	125	reximdv2 3198	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
127	83, 126	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
128	127	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
129	69, 128	pm2.61dne 3030	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
130	129	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
131	130	alrimiv 1931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
132		df-fr 5535	. . . . . . . . . 10 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
133	131, 132	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
134		elun 4079	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
135		elun 4079	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
136	134, 135	anbi12i 626	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) ↔ ((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})))
137		weso 5571	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
138	20, 137	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Or 𝑋)
139		solin 5519	. . . . . . . . . . . . . . 15 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
140	138, 139	sylan 579	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
141		ssun1 4102	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
142	141	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
143	142	ssbrd 5113	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
144		idd 24	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
145	142	ssbrd 5113	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦(𝑊‘𝑋)𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
146	143, 144, 145	3orim123d 1442	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
147	140, 146	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
148	147	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
149		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋))
150	149	ancomd 461	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
151		brxp 5627	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
152	150, 151	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥)
153		ssun2 4103	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
154	153	ssbri 5115	. . . . . . . . . . . . . 14 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)
155		3mix3 1330	. . . . . . . . . . . . . 14 ⊢ (𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
156	152, 154, 155	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
157	156	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
158		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
159		brxp 5627	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
160	158, 159	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
161	153	ssbri 5115	. . . . . . . . . . . . . 14 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
162		3mix1 1328	. . . . . . . . . . . . . 14 ⊢ (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
163	160, 161, 162	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
164	163	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
165		elsni 4575	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑥 = (𝑋𝐹(𝑊‘𝑋)))
166		elsni 4575	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
167		eqtr3 2764	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑋𝐹(𝑊‘𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊‘𝑋))) → 𝑥 = 𝑦)
168	165, 166, 167	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = 𝑦)
169	168	3mix2d 1335	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
170	169	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
171	148, 157, 164, 170	ccased 1035	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
172	136, 171	syl5bi 241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
173	172	ralrimivv 3113	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
174		dfwe2 7602	. . . . . . . . 9 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
175	133, 173, 174	sylanbrc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
176	2	fpwwe2cbv 10317	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(^◡𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
177	176, 4, 13	fpwwe2lem3 10320	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦)
178		cnvimass 5978	. . . . . . . . . . . . . . 15 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
179		fvex 6769	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ∈ V
180		snex 5349	. . . . . . . . . . . . . . . . . 18 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ∈ V
181		xpexg 7578	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊‘𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
182	8, 180, 181	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
183		unexg 7577	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊‘𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
184	179, 182, 183	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
185	184	dmexd 7726	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
186		ssexg 5242	. . . . . . . . . . . . . . 15 ⊢ (((^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∧ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
187	178, 185, 186	sylancr 586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
188	187	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
189		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) → 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}))
190		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
191		simplr 765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
192		nelne2 3041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑋 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
193	190, 191, 192	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
194	87, 166	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
195	194	necon3ai 2967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
196		biorf 933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
197	193, 195, 196	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
198		orcom 866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
199	198, 84	bitr4i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
200	197, 199	bitr2di 287	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ 𝑧(𝑊‘𝑋)𝑦))
201		vex 3426	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
202	201	eliniseg 5991	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
203	202	elv 3428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
204	201	eliniseg 5991	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦))
205	204	elv 3428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦)
206	200, 203, 205	3bitr4g 313	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦})))
207	206	eqrdv 2736	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = (^◡(𝑊‘𝑋) “ {𝑦}))
208	189, 207	sylan9eqr 2801	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = (^◡(𝑊‘𝑋) “ {𝑦}))
209	208	sqxpeqd 5612	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
210	209	ineq2d 4143	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
211		indir 4206	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
212		inxp 5730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})))
213		incom 4131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))})
214		cnvimass 5978	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ dom (𝑊‘𝑋)
215	18	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
216		dmss 5800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
218		dmxpid 5828	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ dom (𝑋 × 𝑋) = 𝑋
219	217, 218	sseqtrdi 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ 𝑋)
220	214, 219	sstrid 3928	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ 𝑋)
221	220, 191	ssneldd 3920	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
222		disjsn 4644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
223	221, 222	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
224	213, 223	eqtrid 2790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ∅)
225	224	xpeq2d 5610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅))
226		xp0 6050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅) = ∅
227	225, 226	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
228	212, 227	eqtrid 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
229	228	uneq2d 4093	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
230	211, 229	eqtrid 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
231		un0 4321	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
232	230, 231	eqtrdi 2795	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
233	232	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
234	210, 233	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
235	208, 234	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))))
236	235	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
237	188, 236	sbcied 3756	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
238	177, 237	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
239	166	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
240	239	eqcomd 2744	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋𝐹(𝑊‘𝑋)) = 𝑦)
241	187	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
242		simplr 765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
243	239	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋)))
244	18	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
245		rnss 5837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
247		df-rn 5591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑊‘𝑋) = dom ^◡(𝑊‘𝑋)
248		rnxpid 6065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑋 × 𝑋) = 𝑋
249	246, 247, 248	3sstr3g 3961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → dom ^◡(𝑊‘𝑋) ⊆ 𝑋)
250	249	sseld 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
251	243, 250	sylbid 239	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
252	242, 251	mtod 197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋))
253		ndmima 6000	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
254	252, 253	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
255	239	sneqd 4570	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊‘𝑋))})
256	255	imaeq2d 5958	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}))
257		df-ima 5593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))})
258		cnvxp 6049	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
259	258	reseq1i 5876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))})
260		ssid 3939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))}
261		xpssres 5917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))} → (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋))
262	260, 261	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
263	259, 262	eqtri 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
264	263	rneqi 5835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
265	46	snnz 4709	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ≠ ∅
266		rnxp 6062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋)
267	265, 266	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋
268	264, 267	eqtri 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
269	257, 268	eqtri 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
270	256, 269	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = 𝑋)
271	254, 270	uneq12d 4094	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
272		cnvun 6035	. . . . . . . . . . . . . . . . . . 19 ⊢ ^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) = (^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
273	272	imaeq1i 5955	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})
274		imaundir 6043	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
275	273, 274	eqtri 2766	. . . . . . . . . . . . . . . . 17 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
276		un0 4321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = 𝑋
277		uncom 4083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
278	276, 277	eqtr3i 2768	. . . . . . . . . . . . . . . . 17 ⊢ 𝑋 = (∅ ∪ 𝑋)
279	271, 275, 278	3eqtr4g 2804	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = 𝑋)
280	189, 279	sylan9eqr 2801	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
281	280	sqxpeqd 5612	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
282	281	ineq2d 4143	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)))
283		indir 4206	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)))
284		df-ss 3900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
285	244, 284	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
286		incom 4131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))})
287		disjsn 4644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
288	242, 287	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
289	286, 288	eqtrid 2790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = ∅)
290	289	xpeq2d 5610	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
291		xpindi 5731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))
292		xp0 6050	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ∅) = ∅
293	290, 291, 292	3eqtr3g 2802	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
294	285, 293	uneq12d 4094	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊‘𝑋) ∪ ∅))
295	283, 294	eqtrid 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊‘𝑋) ∪ ∅))
296		un0 4321	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) ∪ ∅) = (𝑊‘𝑋)
297	295, 296	eqtrdi 2795	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
298	297	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
299	282, 298	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊‘𝑋))
300	280, 299	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊‘𝑋)))
301	300	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
302	241, 301	sbcied 3756	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
303	240, 302	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
304	238, 303	jaodan 954	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
305	135, 304	sylan2b 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
306	305	ralrimiva 3107	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307	175, 306	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
308	2, 3	fpwwe2lem2 10319	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
309	308	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
310	34, 307, 309	mpbir2and 709	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
311	2	relopabiv 5719	. . . . . . 7 ⊢ Rel 𝑊
312	311	releldmi 5846	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊)
313		elssuni 4868	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
314	310, 312, 313	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
315	314, 7	sseqtrrdi 3968	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
316	1, 315	sstrid 3928	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
317	46	snss 4716	. . 3 ⊢ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
318	316, 317	sylibr 233	. 2 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
319	318	pm2.18da 796	1 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∨ w3o 1084 ∧ w3a 1085 ∀wal 1537 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 [wsbc 3711 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 𝒫 cpw 4530 {csn 4558 ∪ cuni 4836 class class class wbr 5070 {copab 5132 Or wor 5493 Fr wfr 5532 We wwe 5534 × cxp 5578 ^◡ccnv 5579 dom cdm 5580 ran crn 5581 ↾ cres 5582 “ cima 5583 Fun wfun 6412 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-oi 9199

This theorem is referenced by: fpwwe2 10330

W3C validator