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 10626

Description: Lemma for fpwwe2 10627. (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 4140	. . . 4 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
2		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3		fpwwe2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4	3	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝐴 ∈ 𝑉)
5		fpwwe2.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
6	5	adantlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7		fpwwe2.4	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ dom 𝑊
8	2, 4, 6, 7	fpwwe2lem11 10625	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
9	2, 4, 6, 7	fpwwe2lem10 10624	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10		ffun 6709	. . . . . . . . . . . . . 14 ⊢ (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11		funfvbrb 7047	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
12	9, 10, 11	3syl 19	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
13	8, 12	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊‘𝑋))
14	2, 4	fpwwe2lem2 10616	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊‘𝑋) ↔ ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
15	13, 14	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
16	15	simpld 499	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)))
17	16	simpld 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ⊆ 𝐴)
18	16	simprd 500	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
19	15	simprd 500	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
20	19	simpld 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) We 𝑋)
21	17, 18, 20	3jca 1144	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋))
22	2, 3, 5	fpwwe2lem4 10618	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
23	21, 22	syldan 602	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
24	23	snssd 4757	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝐴)
25	17, 24	unssd 4153	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴)
26		ssun1 4139	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
27		xpss12 5677	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
28	26, 26, 27	mp2an 704	. . . . . . . . . 10 ⊢ (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
29	18, 28	sstrdi 3957	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
30		xpss12 5677	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
31	26, 1, 30	mp2an 704	. . . . . . . . . 10 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
32	31	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
33	29, 32	unssd 4153	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
34	25, 33	jca 520	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))))
35		ssdif0 4329	. . . . . . . . . . . . . 14 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
36		simpllr 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
37	18	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
38	37	ssbrd 5158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋))))
39		brxp 5711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
40	39	simplbi 501	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
41	38, 40	syl6 36	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
42	36, 41	mtod 201	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)))
43		brxp 5711	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ {(𝑋𝐹(𝑊‘𝑋))}))
44	43	simplbi 501	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
45	36, 44	nsyl 141	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))
46		ovex 7444	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐹(𝑊‘𝑋)) ∈ V
47		breq2 5117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋))))
48		brun 5166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
49	47, 48	bitrdi 290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
50	49	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → (¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
51	46, 50	rexsn 4653	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
52		ioran 999	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
53	51, 52	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
54	42, 45, 53	sylanbrc 594	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
55		sssn 4796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
56	55	bilani 509	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
57		simplrr 789	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ≠ ∅)
58	57	neneqd 2969	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑥 = ∅)
59	56, 58	orcnd 891	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊‘𝑋))})
60	59	raleqdv 3329	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
61		breq1 5116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
62	61	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
63	46, 62	ralsn 4652	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
64	60, 63	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
65	59, 64	rexeqbidv 3346	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
66	54, 65	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
67	66	ex 417	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
68	35, 67	biimtrrid 246	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
69		vex 3467	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
70		difexg 5300	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
71	69, 70	mp1i 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
72		wefr 5652	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
73	20, 72	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Fr 𝑋)
74	73	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑊‘𝑋) Fr 𝑋)
75		simplrl 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
76		uncom 4120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋)
77	75, 76	sseqtrdi 3985	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋))
78		ssundif 4453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
79	77, 78	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
80		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)
81		fri 5620	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
82	71, 74, 79, 80, 81	syl22anc 851	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
83		brun 5166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
84		idd 25	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑊‘𝑋)𝑦 → 𝑧(𝑊‘𝑋)𝑦))
85		brxp 5711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑧 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
86	85	simprbi 502	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
87		eldifn 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
88	87	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
89	88	pm2.21d 122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑧(𝑊‘𝑋)𝑦))
90	86, 89	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑧(𝑊‘𝑋)𝑦))
91	84, 90	jaod 872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) → 𝑧(𝑊‘𝑋)𝑦))
92	83, 91	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → 𝑧(𝑊‘𝑋)𝑦))
93	92	con3d 153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (¬ 𝑧(𝑊‘𝑋)𝑦 → ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
94	93	ralimdv 3185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
95		simpr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
96	95	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
97	18	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
98	97	ssbrd 5158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦))
99		brxp 5711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))
100	99	simplbi 501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
101	98, 100	syl6 36	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
102	96, 101	mtod 201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦)
103		brxp 5711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
104	103	simprbi 502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
105	88, 104	nsyl 141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
106		brun 5166	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
107	61, 106	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
108	107	notbid 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
109	46, 108	ralsn 4652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
110		ioran 999	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
111	109, 110	bitri 278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
112	102, 105, 111	sylanbrc 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
113	94, 112	jctird 535	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
114		ssun1 4139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
115		undif1 4442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
116	114, 115	sseqtrri 3994	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))})
117		ralun 4159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
118		ssralv 4014	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
119	116, 117, 118	mpsyl 69	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
120	113, 119	syl6 36	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
121		eldifi 4093	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 ∈ 𝑥)
122	121	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑦 ∈ 𝑥)
123	120, 122	jctild 534	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
124	123	expimpd 458	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦) → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
125	124	reximdv2 3181	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
126	82, 125	mpd 16	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
127	126	ex 417	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
128	68, 127	pm2.61dne 3050	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
129	128	ex 417	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
130	129	alrimiv 1954	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
131		df-fr 5615	. . . . . . . . . 10 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
132	130, 131	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
133		elun 4115	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
134		elun 4115	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
135	133, 134	anbi12i 639	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) ↔ ((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})))
136		weso 5653	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
137	20, 136	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Or 𝑋)
138		solin 5597	. . . . . . . . . . . . . . 15 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
139	137, 138	sylan 591	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
140		ssun1 4139	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
141	140	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
142	141	ssbrd 5158	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
143		idd 25	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
144	141	ssbrd 5158	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦(𝑊‘𝑋)𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
145	142, 143, 144	3orim123d 1470	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
146	139, 145	mpd 16	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
147	146	ex 417	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
148		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋))
149	148	ancomd 466	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
150		brxp 5711	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
151	149, 150	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥)
152		ssun2 4140	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
153	152	ssbri 5160	. . . . . . . . . . . . . 14 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)
154		3mix3 1349	. . . . . . . . . . . . . 14 ⊢ (𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
155	151, 153, 154	3syl 19	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
156	155	ex 417	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
157		brxp 5711	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
158	157	bilanri 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
159	152	ssbri 5160	. . . . . . . . . . . . . 14 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
160		3mix1 1347	. . . . . . . . . . . . . 14 ⊢ (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
161	158, 159, 160	3syl 19	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
162	161	ex 417	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
163		elsni 4611	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑥 = (𝑋𝐹(𝑊‘𝑋)))
164		elsni 4611	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
165		eqtr3 2791	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑋𝐹(𝑊‘𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊‘𝑋))) → 𝑥 = 𝑦)
166	163, 164, 165	syl2an 607	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = 𝑦)
167	166	3mix2d 1354	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
168	167	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
169	147, 156, 162, 168	ccased 1052	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
170	135, 169	biimtrid 245	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
171	170	ralrimivv 3212	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
172		dfwe2 7772	. . . . . . . . 9 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
173	132, 171, 172	sylanbrc 594	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
174	2	fpwwe2cbv 10614	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(^◡𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
175	174, 4, 13	fpwwe2lem3 10617	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦)
176		cnvimass 6085	. . . . . . . . . . . . . . 15 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
177		fvex 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ∈ V
178		snex 5411	. . . . . . . . . . . . . . . . . 18 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ∈ V
179		xpexg 7748	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊‘𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
180	8, 178, 179	sylancl 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
181		unexg 7741	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊‘𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
182	177, 180, 181	sylancr 598	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
183	182	dmexd 7899	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
184		ssexg 5294	. . . . . . . . . . . . . . 15 ⊢ (((^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∧ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
185	176, 183, 184	sylancr 598	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
186	185	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
187		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) → 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}))
188		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
189		simplr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
190		nelne2 3062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑋 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
191	188, 189, 190	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
192	86, 164	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
193	192	necon3ai 2989	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
194		biorf 949	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
195	191, 193, 194	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
196		orcom 883	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
197	196, 83	bitr4i 281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
198	195, 197	bitr2di 291	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ 𝑧(𝑊‘𝑋)𝑦))
199		vex 3467	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
200	199	eliniseg 6097	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
201	200	elv 3468	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
202	199	eliniseg 6097	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦))
203	202	elv 3468	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦)
204	198, 201, 203	3bitr4g 317	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦})))
205	204	eqrdv 2767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = (^◡(𝑊‘𝑋) “ {𝑦}))
206	187, 205	sylan9eqr 2826	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = (^◡(𝑊‘𝑋) “ {𝑦}))
207	206	sqxpeqd 5694	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
208	207	ineq2d 4181	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
209		indir 4247	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
210		inxp 5819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})))
211		incom 4170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))})
212		cnvimass 6085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ dom (𝑊‘𝑋)
213	18	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
214		dmss 5893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
215	213, 214	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
216		dmxpid 5921	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ dom (𝑋 × 𝑋) = 𝑋
217	215, 216	sseqtrdi 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ 𝑋)
218	212, 217	sstrid 3956	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ 𝑋)
219	218, 189	ssneldd 3948	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
220		disjsn 4682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
221	219, 220	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
222	211, 221	eqtrid 2816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ∅)
223	222	xpeq2d 5692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅))
224		xp0 5762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅) = ∅
225	223, 224	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
226	210, 225	eqtrid 2816	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
227	226	uneq2d 4130	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
228	209, 227	eqtrid 2816	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
229		un0 4358	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
230	228, 229	eqtrdi 2820	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
231	230	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
232	208, 231	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
233	206, 232	oveq12d 7429	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))))
234	233	eqeq1d 2771	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
235	186, 234	sbcied 3796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
236	175, 235	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
237	164	adantl 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
238	237	eqcomd 2775	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋𝐹(𝑊‘𝑋)) = 𝑦)
239	185	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
240		simplr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
241	237	eleq1d 2854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋)))
242	18	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
243		rnss 5930	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
244	242, 243	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
245		df-rn 5673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑊‘𝑋) = dom ^◡(𝑊‘𝑋)
246		rnxpid 6172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑋 × 𝑋) = 𝑋
247	244, 245, 246	3sstr3g 3997	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → dom ^◡(𝑊‘𝑋) ⊆ 𝑋)
248	247	sseld 3944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
249	241, 248	sylbid 243	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
250	240, 249	mtod 201	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋))
251		ndmima 6106	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
252	250, 251	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
253	237	sneqd 4606	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊‘𝑋))})
254	253	imaeq2d 6063	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}))
255		df-ima 5675	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))})
256		cnvxp 6155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
257	256	reseq1i 5975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))})
258		ssid 3967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))}
259		xpssres 6018	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))} → (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋))
260	258, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
261	257, 260	eqtri 2792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
262	261	rneqi 5928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
263	46	snnz 4747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ≠ ∅
264		rnxp 6169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋)
265	263, 264	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋
266	262, 265	eqtri 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
267	255, 266	eqtri 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
268	254, 267	eqtrdi 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = 𝑋)
269	252, 268	uneq12d 4131	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
270		cnvun 6140	. . . . . . . . . . . . . . . . . . 19 ⊢ ^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) = (^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
271	270	imaeq1i 6060	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})
272		imaundir 6149	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
273	271, 272	eqtri 2792	. . . . . . . . . . . . . . . . 17 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
274		un0 4358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = 𝑋
275		uncom 4120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
276	274, 275	eqtr3i 2794	. . . . . . . . . . . . . . . . 17 ⊢ 𝑋 = (∅ ∪ 𝑋)
277	269, 273, 276	3eqtr4g 2829	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = 𝑋)
278	187, 277	sylan9eqr 2826	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
279	278	sqxpeqd 5694	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
280	279	ineq2d 4181	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)))
281		indir 4247	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)))
282		dfss2 3931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
283	242, 282	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
284		incom 4170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))})
285		disjsn 4682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
286	240, 285	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
287	284, 286	eqtrid 2816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = ∅)
288	287	xpeq2d 5692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
289		xpindi 5820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))
290		xp0 5762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ∅) = ∅
291	288, 289, 290	3eqtr3g 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
292	283, 291	uneq12d 4131	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊‘𝑋) ∪ ∅))
293	281, 292	eqtrid 2816	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊‘𝑋) ∪ ∅))
294		un0 4358	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) ∪ ∅) = (𝑊‘𝑋)
295	293, 294	eqtrdi 2820	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
296	295	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
297	280, 296	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊‘𝑋))
298	278, 297	oveq12d 7429	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊‘𝑋)))
299	298	eqeq1d 2771	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
300	239, 299	sbcied 3796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
301	238, 300	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
302	236, 301	jaodan 972	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
303	134, 302	sylan2b 605	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
304	303	ralrimiva 3163	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
305	173, 304	jca 520	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
306	2, 3	fpwwe2lem2 10616	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
307	306	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
308	34, 305, 307	mpbir2and 725	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
309	2	relopabiv 5808	. . . . . . 7 ⊢ Rel 𝑊
310	309	releldmi 5939	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊)
311		elssuni 4908	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
312	308, 310, 311	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
313	312, 7	sseqtrrdi 3986	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
314	1, 313	sstrid 3956	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
315	46	snss 4755	. . 3 ⊢ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
316	314, 315	sylibr 237	. 2 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
317	316	pm2.18da 811	1 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∨ w3o 1100 ∧ w3a 1101 ∀wal 1565 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 Vcvv 3463 [wsbc 3753 ∖ cdif 3910 ∪ cun 3911 ∩ cin 3912 ⊆ wss 3913 ∅c0 4294 𝒫 cpw 4567 {csn 4594 ∪ cuni 4876 class class class wbr 5113 {copab 5177 Or wor 5569 Fr wfr 5612 We wwe 5614 × cxp 5660 ^◡ccnv 5661 dom cdm 5662 ran crn 5663 ↾ cres 5664 “ cima 5665 Fun wfun 6531 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-oi 9471

This theorem is referenced by: fpwwe2 10627

W3C validator