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 10578

Description: Lemma for fpwwe2 10579. (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 4133	. . . 4 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
2		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3		fpwwe2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4	3	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝐴 ∈ 𝑉)
5		fpwwe2.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
6	5	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7		fpwwe2.4	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ dom 𝑊
8	2, 4, 6, 7	fpwwe2lem11 10577	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
9	2, 4, 6, 7	fpwwe2lem10 10576	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10		ffun 6671	. . . . . . . . . . . . . 14 ⊢ (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11		funfvbrb 7001	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
12	9, 10, 11	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
13	8, 12	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊‘𝑋))
14	2, 4	fpwwe2lem2 10568	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊‘𝑋) ↔ ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
15	13, 14	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
16	15	simpld 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)))
17	16	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ⊆ 𝐴)
18	16	simprd 496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
19	15	simprd 496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
20	19	simpld 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) We 𝑋)
21	17, 18, 20	3jca 1128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋))
22	2, 3, 5	fpwwe2lem4 10570	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
23	21, 22	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
24	23	snssd 4769	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝐴)
25	17, 24	unssd 4146	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴)
26		ssun1 4132	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
27		xpss12 5648	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
28	26, 26, 27	mp2an 690	. . . . . . . . . 10 ⊢ (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
29	18, 28	sstrdi 3956	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
30		xpss12 5648	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
31	26, 1, 30	mp2an 690	. . . . . . . . . 10 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
32	31	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
33	29, 32	unssd 4146	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
34	25, 33	jca 512	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))))
35		ssdif0 4323	. . . . . . . . . . . . . 14 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
36		simpllr 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
37	18	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
38	37	ssbrd 5148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋))))
39		brxp 5681	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
40	39	simplbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
41	38, 40	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
42	36, 41	mtod 197	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)))
43		brxp 5681	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ {(𝑋𝐹(𝑊‘𝑋))}))
44	43	simplbi 498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
45	36, 44	nsyl 140	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))
46		ovex 7390	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐹(𝑊‘𝑋)) ∈ V
47		breq2 5109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋))))
48		brun 5156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
49	47, 48	bitrdi 286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
50	49	notbid 317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → (¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
51	46, 50	rexsn 4643	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
52		ioran 982	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
53	51, 52	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
54	42, 45, 53	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
55		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))})
56		sssn 4786	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
57	55, 56	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
58		simplrr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ≠ ∅)
59	58	neneqd 2948	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑥 = ∅)
60	57, 59	orcnd 877	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊‘𝑋))})
61	60	raleqdv 3313	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
62		breq1 5108	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
63	62	notbid 317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
64	46, 63	ralsn 4642	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
65	61, 64	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
66	60, 65	rexeqbidv 3320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
67	54, 66	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
68	67	ex 413	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
69	35, 68	biimtrrid 242	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
70		vex 3449	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
71		difexg 5284	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
72	70, 71	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
73		wefr 5623	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
74	20, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Fr 𝑋)
75	74	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑊‘𝑋) Fr 𝑋)
76		simplrl 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
77		uncom 4113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋)
78	76, 77	sseqtrdi 3994	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋))
79		ssundif 4445	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
80	78, 79	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
81		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)
82		fri 5593	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
83	72, 75, 80, 81, 82	syl22anc 837	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
84		brun 5156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
85		idd 24	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑊‘𝑋)𝑦 → 𝑧(𝑊‘𝑋)𝑦))
86		brxp 5681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑧 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
87	86	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
88		eldifn 4087	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
89	88	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
90	89	pm2.21d 121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑧(𝑊‘𝑋)𝑦))
91	87, 90	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑧(𝑊‘𝑋)𝑦))
92	85, 91	jaod 857	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) → 𝑧(𝑊‘𝑋)𝑦))
93	84, 92	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → 𝑧(𝑊‘𝑋)𝑦))
94	93	con3d 152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (¬ 𝑧(𝑊‘𝑋)𝑦 → ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
95	94	ralimdv 3166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
96		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
97	96	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
98	18	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
99	98	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦))
100		brxp 5681	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))
101	100	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
102	99, 101	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
103	97, 102	mtod 197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦)
104		brxp 5681	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
105	104	simprbi 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
106	89, 105	nsyl 140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
107		brun 5156	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
108	62, 107	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
109	108	notbid 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
110	46, 109	ralsn 4642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
111		ioran 982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
112	110, 111	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
113	103, 106, 112	sylanbrc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
114	95, 113	jctird 527	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
115		ssun1 4132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
116		undif1 4435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
117	115, 116	sseqtrri 3981	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))})
118		ralun 4152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
119		ssralv 4010	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
120	117, 118, 119	mpsyl 68	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
121	114, 120	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
122		eldifi 4086	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 ∈ 𝑥)
123	122	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑦 ∈ 𝑥)
124	121, 123	jctild 526	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
125	124	expimpd 454	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦) → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
126	125	reximdv2 3161	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
127	83, 126	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
128	127	ex 413	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
129	69, 128	pm2.61dne 3031	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
130	129	ex 413	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
131	130	alrimiv 1930	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
132		df-fr 5588	. . . . . . . . . 10 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
133	131, 132	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
134		elun 4108	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
135		elun 4108	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
136	134, 135	anbi12i 627	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) ↔ ((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})))
137		weso 5624	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
138	20, 137	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Or 𝑋)
139		solin 5570	. . . . . . . . . . . . . . 15 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
140	138, 139	sylan 580	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
141		ssun1 4132	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
142	141	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
143	142	ssbrd 5148	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
144		idd 24	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
145	142	ssbrd 5148	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦(𝑊‘𝑋)𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
146	143, 144, 145	3orim123d 1444	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
147	140, 146	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
148	147	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
149		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋))
150	149	ancomd 462	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
151		brxp 5681	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
152	150, 151	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥)
153		ssun2 4133	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
154	153	ssbri 5150	. . . . . . . . . . . . . 14 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)
155		3mix3 1332	. . . . . . . . . . . . . 14 ⊢ (𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
156	152, 154, 155	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
157	156	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
158		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
159		brxp 5681	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
160	158, 159	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
161	153	ssbri 5150	. . . . . . . . . . . . . 14 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
162		3mix1 1330	. . . . . . . . . . . . . 14 ⊢ (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
163	160, 161, 162	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
164	163	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
165		elsni 4603	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑥 = (𝑋𝐹(𝑊‘𝑋)))
166		elsni 4603	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
167		eqtr3 2762	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑋𝐹(𝑊‘𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊‘𝑋))) → 𝑥 = 𝑦)
168	165, 166, 167	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = 𝑦)
169	168	3mix2d 1337	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
170	169	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
171	148, 157, 164, 170	ccased 1037	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
172	136, 171	biimtrid 241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
173	172	ralrimivv 3195	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
174		dfwe2 7708	. . . . . . . . 9 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
175	133, 173, 174	sylanbrc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
176	2	fpwwe2cbv 10566	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(^◡𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
177	176, 4, 13	fpwwe2lem3 10569	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦)
178		cnvimass 6033	. . . . . . . . . . . . . . 15 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
179		fvex 6855	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ∈ V
180		snex 5388	. . . . . . . . . . . . . . . . . 18 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ∈ V
181		xpexg 7684	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊‘𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
182	8, 180, 181	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
183		unexg 7683	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊‘𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
184	179, 182, 183	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
185	184	dmexd 7842	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
186		ssexg 5280	. . . . . . . . . . . . . . 15 ⊢ (((^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∧ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
187	178, 185, 186	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
188	187	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
189		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) → 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}))
190		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
191		simplr 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
192		nelne2 3042	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑋 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
193	190, 191, 192	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
194	87, 166	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
195	194	necon3ai 2968	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
196		biorf 935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
197	193, 195, 196	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
198		orcom 868	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
199	198, 84	bitr4i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
200	197, 199	bitr2di 287	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ 𝑧(𝑊‘𝑋)𝑦))
201		vex 3449	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
202	201	eliniseg 6046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
203	202	elv 3451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
204	201	eliniseg 6046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦))
205	204	elv 3451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦)
206	200, 203, 205	3bitr4g 313	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦})))
207	206	eqrdv 2734	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = (^◡(𝑊‘𝑋) “ {𝑦}))
208	189, 207	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = (^◡(𝑊‘𝑋) “ {𝑦}))
209	208	sqxpeqd 5665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
210	209	ineq2d 4172	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
211		indir 4235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
212		inxp 5788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})))
213		incom 4161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))})
214		cnvimass 6033	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ dom (𝑊‘𝑋)
215	18	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
216		dmss 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
218		dmxpid 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ dom (𝑋 × 𝑋) = 𝑋
219	217, 218	sseqtrdi 3994	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ 𝑋)
220	214, 219	sstrid 3955	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ 𝑋)
221	220, 191	ssneldd 3947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
222		disjsn 4672	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
223	221, 222	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
224	213, 223	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ∅)
225	224	xpeq2d 5663	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅))
226		xp0 6110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅) = ∅
227	225, 226	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
228	212, 227	eqtrid 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
229	228	uneq2d 4123	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
230	211, 229	eqtrid 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
231		un0 4350	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
232	230, 231	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
233	232	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
234	210, 233	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
235	208, 234	oveq12d 7375	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))))
236	235	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
237	188, 236	sbcied 3784	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
238	177, 237	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
239	166	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
240	239	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋𝐹(𝑊‘𝑋)) = 𝑦)
241	187	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
242		simplr 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
243	239	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋)))
244	18	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
245		rnss 5894	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
247		df-rn 5644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑊‘𝑋) = dom ^◡(𝑊‘𝑋)
248		rnxpid 6125	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑋 × 𝑋) = 𝑋
249	246, 247, 248	3sstr3g 3988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → dom ^◡(𝑊‘𝑋) ⊆ 𝑋)
250	249	sseld 3943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
251	243, 250	sylbid 239	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
252	242, 251	mtod 197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋))
253		ndmima 6055	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
254	252, 253	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
255	239	sneqd 4598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊‘𝑋))})
256	255	imaeq2d 6013	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}))
257		df-ima 5646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))})
258		cnvxp 6109	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
259	258	reseq1i 5933	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))})
260		ssid 3966	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))}
261		xpssres 5974	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))} → (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋))
262	260, 261	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
263	259, 262	eqtri 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
264	263	rneqi 5892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
265	46	snnz 4737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ≠ ∅
266		rnxp 6122	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋)
267	265, 266	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋
268	264, 267	eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
269	257, 268	eqtri 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
270	256, 269	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = 𝑋)
271	254, 270	uneq12d 4124	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
272		cnvun 6095	. . . . . . . . . . . . . . . . . . 19 ⊢ ^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) = (^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
273	272	imaeq1i 6010	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})
274		imaundir 6103	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
275	273, 274	eqtri 2764	. . . . . . . . . . . . . . . . 17 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
276		un0 4350	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = 𝑋
277		uncom 4113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
278	276, 277	eqtr3i 2766	. . . . . . . . . . . . . . . . 17 ⊢ 𝑋 = (∅ ∪ 𝑋)
279	271, 275, 278	3eqtr4g 2801	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = 𝑋)
280	189, 279	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
281	280	sqxpeqd 5665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
282	281	ineq2d 4172	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)))
283		indir 4235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)))
284		df-ss 3927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
285	244, 284	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
286		incom 4161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))})
287		disjsn 4672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
288	242, 287	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
289	286, 288	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = ∅)
290	289	xpeq2d 5663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
291		xpindi 5789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))
292		xp0 6110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ∅) = ∅
293	290, 291, 292	3eqtr3g 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
294	285, 293	uneq12d 4124	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊‘𝑋) ∪ ∅))
295	283, 294	eqtrid 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊‘𝑋) ∪ ∅))
296		un0 4350	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) ∪ ∅) = (𝑊‘𝑋)
297	295, 296	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
298	297	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
299	282, 298	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊‘𝑋))
300	280, 299	oveq12d 7375	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊‘𝑋)))
301	300	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
302	241, 301	sbcied 3784	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
303	240, 302	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
304	238, 303	jaodan 956	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
305	135, 304	sylan2b 594	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
306	305	ralrimiva 3143	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307	175, 306	jca 512	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
308	2, 3	fpwwe2lem2 10568	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
309	308	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
310	34, 307, 309	mpbir2and 711	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
311	2	relopabiv 5776	. . . . . . 7 ⊢ Rel 𝑊
312	311	releldmi 5903	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊)
313		elssuni 4898	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
314	310, 312, 313	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
315	314, 7	sseqtrrdi 3995	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
316	1, 315	sstrid 3955	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
317	46	snss 4746	. . 3 ⊢ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
318	316, 317	sylibr 233	. 2 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
319	318	pm2.18da 798	1 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∨ w3o 1086 ∧ w3a 1087 ∀wal 1539 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 Vcvv 3445 [wsbc 3739 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 𝒫 cpw 4560 {csn 4586 ∪ cuni 4865 class class class wbr 5105 {copab 5167 Or wor 5544 Fr wfr 5585 We wwe 5587 × cxp 5631 ^◡ccnv 5632 dom cdm 5633 ran crn 5634 ↾ cres 5635 “ cima 5636 Fun wfun 6490 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-oi 9446

This theorem is referenced by: fpwwe2 10579

W3C validator