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 10398

Description: Lemma for fpwwe2 10399. (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 4107	. . . 4 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
2		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3		fpwwe2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4	3	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝐴 ∈ 𝑉)
5		fpwwe2.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
6	5	adantlr 712	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7		fpwwe2.4	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ dom 𝑊
8	2, 4, 6, 7	fpwwe2lem11 10397	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
9	2, 4, 6, 7	fpwwe2lem10 10396	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10		ffun 6603	. . . . . . . . . . . . . 14 ⊢ (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11		funfvbrb 6928	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
12	9, 10, 11	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
13	8, 12	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊‘𝑋))
14	2, 4	fpwwe2lem2 10388	. . . . . . . . . . . 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 1127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋))
22	2, 3, 5	fpwwe2lem4 10390	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
23	21, 22	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
24	23	snssd 4742	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝐴)
25	17, 24	unssd 4120	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴)
26		ssun1 4106	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
27		xpss12 5604	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
28	26, 26, 27	mp2an 689	. . . . . . . . . 10 ⊢ (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
29	18, 28	sstrdi 3933	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
30		xpss12 5604	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
31	26, 1, 30	mp2an 689	. . . . . . . . . 10 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
32	31	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
33	29, 32	unssd 4120	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
34	25, 33	jca 512	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))))
35		ssdif0 4297	. . . . . . . . . . . . . 14 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
36		simpllr 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
37	18	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
38	37	ssbrd 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋))))
39		brxp 5636	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
40	39	simplbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
41	38, 40	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
42	36, 41	mtod 197	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)))
43		brxp 5636	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ {(𝑋𝐹(𝑊‘𝑋))}))
44	43	simplbi 498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
45	36, 44	nsyl 140	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))
46		ovex 7308	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐹(𝑊‘𝑋)) ∈ V
47		breq2 5078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋))))
48		brun 5125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
49	47, 48	bitrdi 287	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
50	49	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → (¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
51	46, 50	rexsn 4618	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
52		ioran 981	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
53	51, 52	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
54	42, 45, 53	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
55		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))})
56		sssn 4759	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
57	55, 56	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
58		simplrr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ≠ ∅)
59	58	neneqd 2948	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑥 = ∅)
60	57, 59	orcnd 876	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊‘𝑋))})
61	60	raleqdv 3348	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
62		breq1 5077	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
63	62	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
64	46, 63	ralsn 4617	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
65	61, 64	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
66	60, 65	rexeqbidv 3337	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
67	54, 66	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
68	67	ex 413	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
69	35, 68	syl5bir 242	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
70		vex 3436	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
71		difexg 5251	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
72	70, 71	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
73		wefr 5579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
74	20, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Fr 𝑋)
75	74	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑊‘𝑋) Fr 𝑋)
76		simplrl 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
77		uncom 4087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋)
78	76, 77	sseqtrdi 3971	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋))
79		ssundif 4418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
80	78, 79	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
81		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)
82		fri 5549	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
83	72, 75, 80, 81, 82	syl22anc 836	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
84		brun 5125	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
85		idd 24	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑊‘𝑋)𝑦 → 𝑧(𝑊‘𝑋)𝑦))
86		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑧 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
87	86	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
88		eldifn 4062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
89	88	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
90	89	pm2.21d 121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑧(𝑊‘𝑋)𝑦))
91	87, 90	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑧(𝑊‘𝑋)𝑦))
92	85, 91	jaod 856	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) → 𝑧(𝑊‘𝑋)𝑦))
93	84, 92	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → 𝑧(𝑊‘𝑋)𝑦))
94	93	con3d 152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (¬ 𝑧(𝑊‘𝑋)𝑦 → ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
95	94	ralimdv 3109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
96		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
97	96	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
98	18	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
99	98	ssbrd 5117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦))
100		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))
101	100	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
102	99, 101	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
103	97, 102	mtod 197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦)
104		brxp 5636	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
105	104	simprbi 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
106	89, 105	nsyl 140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
107		brun 5125	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
108	62, 107	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
109	108	notbid 318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
110	46, 109	ralsn 4617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
111		ioran 981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
112	110, 111	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
113	103, 106, 112	sylanbrc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
114	95, 113	jctird 527	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
115		ssun1 4106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
116		undif1 4409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
117	115, 116	sseqtrri 3958	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))})
118		ralun 4126	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
119		ssralv 3987	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
120	117, 118, 119	mpsyl 68	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
121	114, 120	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
122		eldifi 4061	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 ∈ 𝑥)
123	122	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑦 ∈ 𝑥)
124	121, 123	jctild 526	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
125	124	expimpd 454	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦) → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
126	125	reximdv2 3199	. . . . . . . . . . . . . . 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 5544	. . . . . . . . . 10 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
133	131, 132	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
134		elun 4083	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
135		elun 4083	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
136	134, 135	anbi12i 627	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) ↔ ((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})))
137		weso 5580	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
138	20, 137	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Or 𝑋)
139		solin 5528	. . . . . . . . . . . . . . 15 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
140	138, 139	sylan 580	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
141		ssun1 4106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
142	141	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
143	142	ssbrd 5117	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
144		idd 24	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
145	142	ssbrd 5117	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦(𝑊‘𝑋)𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
146	143, 144, 145	3orim123d 1443	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
147	140, 146	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
148	147	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
149		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋))
150	149	ancomd 462	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
151		brxp 5636	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
152	150, 151	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥)
153		ssun2 4107	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
154	153	ssbri 5119	. . . . . . . . . . . . . 14 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)
155		3mix3 1331	. . . . . . . . . . . . . 14 ⊢ (𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
156	152, 154, 155	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
157	156	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
158		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
159		brxp 5636	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
160	158, 159	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
161	153	ssbri 5119	. . . . . . . . . . . . . 14 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
162		3mix1 1329	. . . . . . . . . . . . . 14 ⊢ (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
163	160, 161, 162	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
164	163	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
165		elsni 4578	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑥 = (𝑋𝐹(𝑊‘𝑋)))
166		elsni 4578	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
167		eqtr3 2764	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑋𝐹(𝑊‘𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊‘𝑋))) → 𝑥 = 𝑦)
168	165, 166, 167	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = 𝑦)
169	168	3mix2d 1336	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
170	169	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
171	148, 157, 164, 170	ccased 1036	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
172	136, 171	syl5bi 241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
173	172	ralrimivv 3122	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
174		dfwe2 7624	. . . . . . . . 9 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
175	133, 173, 174	sylanbrc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
176	2	fpwwe2cbv 10386	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(^◡𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
177	176, 4, 13	fpwwe2lem3 10389	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦)
178		cnvimass 5989	. . . . . . . . . . . . . . 15 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
179		fvex 6787	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ∈ V
180		snex 5354	. . . . . . . . . . . . . . . . . 18 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ∈ V
181		xpexg 7600	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊‘𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
182	8, 180, 181	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
183		unexg 7599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊‘𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
184	179, 182, 183	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
185	184	dmexd 7752	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
186		ssexg 5247	. . . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . . . . . . . . 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 934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
197	193, 195, 196	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
198		orcom 867	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
199	198, 84	bitr4i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
200	197, 199	bitr2di 288	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ 𝑧(𝑊‘𝑋)𝑦))
201		vex 3436	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
202	201	eliniseg 6002	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
203	202	elv 3438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
204	201	eliniseg 6002	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦))
205	204	elv 3438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦)
206	200, 203, 205	3bitr4g 314	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦})))
207	206	eqrdv 2736	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = (^◡(𝑊‘𝑋) “ {𝑦}))
208	189, 207	sylan9eqr 2800	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = (^◡(𝑊‘𝑋) “ {𝑦}))
209	208	sqxpeqd 5621	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
210	209	ineq2d 4146	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
211		indir 4209	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
212		inxp 5741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})))
213		incom 4135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))})
214		cnvimass 5989	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ dom (𝑊‘𝑋)
215	18	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
216		dmss 5811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
218		dmxpid 5839	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ dom (𝑋 × 𝑋) = 𝑋
219	217, 218	sseqtrdi 3971	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ 𝑋)
220	214, 219	sstrid 3932	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ 𝑋)
221	220, 191	ssneldd 3924	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
222		disjsn 4647	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
223	221, 222	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
224	213, 223	eqtrid 2790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ∅)
225	224	xpeq2d 5619	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅))
226		xp0 6061	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅) = ∅
227	225, 226	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
228	212, 227	eqtrid 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
229	228	uneq2d 4097	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
230	211, 229	eqtrid 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
231		un0 4324	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
232	230, 231	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
233	232	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
234	210, 233	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
235	208, 234	oveq12d 7293	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))))
236	235	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
237	188, 236	sbcied 3761	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
238	177, 237	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
239	166	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
240	239	eqcomd 2744	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋𝐹(𝑊‘𝑋)) = 𝑦)
241	187	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
242		simplr 766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
243	239	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋)))
244	18	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
245		rnss 5848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
247		df-rn 5600	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑊‘𝑋) = dom ^◡(𝑊‘𝑋)
248		rnxpid 6076	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑋 × 𝑋) = 𝑋
249	246, 247, 248	3sstr3g 3965	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → dom ^◡(𝑊‘𝑋) ⊆ 𝑋)
250	249	sseld 3920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
251	243, 250	sylbid 239	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
252	242, 251	mtod 197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋))
253		ndmima 6011	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
254	252, 253	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
255	239	sneqd 4573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊‘𝑋))})
256	255	imaeq2d 5969	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}))
257		df-ima 5602	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))})
258		cnvxp 6060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
259	258	reseq1i 5887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))})
260		ssid 3943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))}
261		xpssres 5928	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))} → (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋))
262	260, 261	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
263	259, 262	eqtri 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
264	263	rneqi 5846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
265	46	snnz 4712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ≠ ∅
266		rnxp 6073	. . . . . . . . . . . . . . . . . . . . . 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 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = 𝑋)
271	254, 270	uneq12d 4098	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
272		cnvun 6046	. . . . . . . . . . . . . . . . . . 19 ⊢ ^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) = (^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
273	272	imaeq1i 5966	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})
274		imaundir 6054	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
275	273, 274	eqtri 2766	. . . . . . . . . . . . . . . . 17 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
276		un0 4324	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = 𝑋
277		uncom 4087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
278	276, 277	eqtr3i 2768	. . . . . . . . . . . . . . . . 17 ⊢ 𝑋 = (∅ ∪ 𝑋)
279	271, 275, 278	3eqtr4g 2803	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = 𝑋)
280	189, 279	sylan9eqr 2800	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
281	280	sqxpeqd 5621	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
282	281	ineq2d 4146	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)))
283		indir 4209	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)))
284		df-ss 3904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
285	244, 284	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
286		incom 4135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))})
287		disjsn 4647	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
288	242, 287	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
289	286, 288	eqtrid 2790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = ∅)
290	289	xpeq2d 5619	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
291		xpindi 5742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))
292		xp0 6061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ∅) = ∅
293	290, 291, 292	3eqtr3g 2801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
294	285, 293	uneq12d 4098	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊‘𝑋) ∪ ∅))
295	283, 294	eqtrid 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊‘𝑋) ∪ ∅))
296		un0 4324	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) ∪ ∅) = (𝑊‘𝑋)
297	295, 296	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
298	297	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
299	282, 298	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊‘𝑋))
300	280, 299	oveq12d 7293	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊‘𝑋)))
301	300	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
302	241, 301	sbcied 3761	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
303	240, 302	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
304	238, 303	jaodan 955	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
305	135, 304	sylan2b 594	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
306	305	ralrimiva 3103	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307	175, 306	jca 512	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
308	2, 3	fpwwe2lem2 10388	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
309	308	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
310	34, 307, 309	mpbir2and 710	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
311	2	relopabiv 5730	. . . . . . 7 ⊢ Rel 𝑊
312	311	releldmi 5857	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊)
313		elssuni 4871	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
314	310, 312, 313	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
315	314, 7	sseqtrrdi 3972	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
316	1, 315	sstrid 3932	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
317	46	snss 4719	. . 3 ⊢ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
318	316, 317	sylibr 233	. 2 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
319	318	pm2.18da 797	1 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)

Colors of variables: wff setvar class

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

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

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

This theorem is referenced by: fpwwe2 10399

W3C validator