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 10556

Description: Lemma for fpwwe2 10557. (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 4108	. . . 4 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
2		fpwwe2.1	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3		fpwwe2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4	3	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝐴 ∈ 𝑉)
5		fpwwe2.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
6	5	adantlr 721	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7		fpwwe2.4	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ dom 𝑊
8	2, 4, 6, 7	fpwwe2lem11 10555	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
9	2, 4, 6, 7	fpwwe2lem10 10554	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10		ffun 6658	. . . . . . . . . . . . . 14 ⊢ (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11		funfvbrb 6992	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
12	9, 10, 11	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
13	8, 12	mpbid 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊‘𝑋))
14	2, 4	fpwwe2lem2 10546	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊‘𝑋) ↔ ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
15	13, 14	mpbid 233	. . . . . . . . . . 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 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋))
22	2, 3, 5	fpwwe2lem4 10548	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊‘𝑋) We 𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
23	21, 22	syldan 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝐴)
24	23	snssd 4718	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝐴)
25	17, 24	unssd 4121	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴)
26		ssun1 4107	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})
27		xpss12 5633	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
28	26, 26, 27	mp2an 698	. . . . . . . . . 10 ⊢ (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
29	18, 28	sstrdi 3927	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
30		xpss12 5633	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ {(𝑋𝐹(𝑊‘𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
31	26, 1, 30	mp2an 698	. . . . . . . . . 10 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
32	31	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
33	29, 32	unssd 4121	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})))
34	25, 33	jca 516	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))))
35		ssdif0 4294	. . . . . . . . . . . . . 14 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
36		simpllr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
37	18	ad2antrr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
38	37	ssbrd 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋))))
39		brxp 5667	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
40	39	simplbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
41	38, 40	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
42	36, 41	mtod 199	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)))
43		brxp 5667	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ {(𝑋𝐹(𝑊‘𝑋))}))
44	43	simplbi 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
45	36, 44	nsyl 140	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))
46		ovex 7389	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋𝐹(𝑊‘𝑋)) ∈ V
47		breq2 5076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋))))
48		brun 5123	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))(𝑋𝐹(𝑊‘𝑋)) ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
49	47, 48	bitrdi 288	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
50	49	notbid 319	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑋𝐹(𝑊‘𝑋)) → (¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋)))))
51	46, 50	rexsn 4614	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
52		ioran 991	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
53	51, 52	bitri 276	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)(𝑋𝐹(𝑊‘𝑋)) ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})(𝑋𝐹(𝑊‘𝑋))))
54	42, 45, 53	sylanbrc 589	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
55		sssn 4757	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
56	55	bilani 505	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊‘𝑋))}))
57		simplrr 783	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 ≠ ∅)
58	57	neneqd 2939	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑥 = ∅)
59	56, 58	orcnd 884	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊‘𝑋))})
60	59	raleqdv 3297	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
61		breq1 5075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
62	61	notbid 319	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
63	46, 62	ralsn 4613	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
64	60, 63	bitrdi 288	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
65	59, 64	rexeqbidv 3314	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → (∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ (𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
66	54, 65	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))}) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
67	66	ex 413	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊‘𝑋))} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
68	35, 67	biimtrrid 244	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
69		vex 3435	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
70		difexg 5257	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
71	69, 70	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
72		wefr 5608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
73	20, 72	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Fr 𝑋)
74	73	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑊‘𝑋) Fr 𝑋)
75		simplrl 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
76		uncom 4088	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋)
77	75, 76	sseqtrdi 3955	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋))
78		ssundif 4415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ⊆ ({(𝑋𝐹(𝑊‘𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
79	77, 78	sylib 219	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
80		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)
81		fri 5576	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
82	71, 74, 79, 80, 81	syl22anc 844	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦)
83		brun 5123	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
84		idd 24	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑊‘𝑋)𝑦 → 𝑧(𝑊‘𝑋)𝑦))
85		brxp 5667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑧 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
86	85	simprbi 498	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
87		eldifn 4062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
88	87	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
89	88	pm2.21d 121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑧(𝑊‘𝑋)𝑦))
90	86, 89	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑧(𝑊‘𝑋)𝑦))
91	84, 90	jaod 865	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) → 𝑧(𝑊‘𝑋)𝑦))
92	83, 91	biimtrid 243	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → 𝑧(𝑊‘𝑋)𝑦))
93	92	con3d 152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (¬ 𝑧(𝑊‘𝑋)𝑦 → ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
94	93	ralimdv 3153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
95		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
96	95	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
97	18	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
98	97	ssbrd 5115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦))
99		brxp 5667	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))
100	99	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
101	98, 100	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
102	96, 101	mtod 199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦)
103		brxp 5667	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
104	103	simprbi 498	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})
105	88, 104	nsyl 140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
106		brun 5123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋𝐹(𝑊‘𝑋))((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
107	61, 106	bitrdi 288	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
108	107	notbid 319	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑋𝐹(𝑊‘𝑋)) → (¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)))
109	46, 108	ralsn 4613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
110		ioran 991	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∨ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
111	109, 110	bitri 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊‘𝑋))(𝑊‘𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊‘𝑋))(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
112	102, 105, 111	sylanbrc 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
113	94, 112	jctird 531	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
114		ssun1 4107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
115		undif1 4404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊‘𝑋))})
116	114, 115	sseqtrri 3964	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))})
117		ralun 4127	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
118		ssralv 3983	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∪ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
119	116, 117, 118	mpsyl 68	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊‘𝑋))} ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦) → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
120	113, 119	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
121		eldifi 4061	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 ∈ 𝑥)
122	121	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑦 ∈ 𝑥)
123	120, 122	jctild 530	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
124	123	expimpd 454	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦) → (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)))
125	124	reximdv2 3149	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ¬ 𝑧(𝑊‘𝑋)𝑦 → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
126	82, 125	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
127	126	ex 413	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊‘𝑋))}) ≠ ∅ → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
128	68, 127	pm2.61dne 3020	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
129	128	ex 413	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
130	129	alrimiv 1934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
131		df-fr 5571	. . . . . . . . . 10 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
132	130, 131	sylibr 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
133		elun 4083	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
134		elun 4083	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
135	133, 134	anbi12i 634	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) ↔ ((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})))
136		weso 5609	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
137	20, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑊‘𝑋) Or 𝑋)
138		solin 5553	. . . . . . . . . . . . . . 15 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
139	137, 138	sylan 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥))
140		ssun1 4107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
141	140	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑊‘𝑋) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
142	141	ssbrd 5115	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑊‘𝑋)𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
143		idd 24	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
144	141	ssbrd 5115	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦(𝑊‘𝑋)𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
145	142, 143, 144	3orim123d 1452	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑊‘𝑋)𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦(𝑊‘𝑋)𝑥) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
146	139, 145	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
147	146	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
148		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋))
149	148	ancomd 462	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
150		brxp 5667	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
151	149, 150	sylibr 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥)
152		ssun2 4108	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
153	152	ssbri 5117	. . . . . . . . . . . . . 14 ⊢ (𝑦(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑥 → 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)
154		3mix3 1339	. . . . . . . . . . . . . 14 ⊢ (𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
155	151, 153, 154	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋)) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
156	155	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ 𝑋) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
157		brxp 5667	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}))
158	157	bilanri 507	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
159	152	ssbri 5117	. . . . . . . . . . . . . 14 ⊢ (𝑥(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
160		3mix1 1337	. . . . . . . . . . . . . 14 ⊢ (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
161	158, 159, 160	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
162	161	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
163		elsni 4572	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑥 = (𝑋𝐹(𝑊‘𝑋)))
164		elsni 4572	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))} → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
165		eqtr3 2761	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑋𝐹(𝑊‘𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊‘𝑋))) → 𝑥 = 𝑦)
166	163, 164, 165	syl2an 602	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑥 = 𝑦)
167	166	3mix2d 1344	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
168	167	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
169	147, 156, 162, 168	ccased 1044	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑥 ∈ 𝑋 ∨ 𝑥 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
170	135, 169	biimtrid 243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → (𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
171	170	ralrimivv 3180	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥))
172		dfwe2 7717	. . . . . . . . 9 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ↔ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})(𝑥((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑥)))
173	132, 171, 172	sylanbrc 589	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))
174	2	fpwwe2cbv 10544	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(^◡𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
175	174, 4, 13	fpwwe2lem3 10547	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦)
176		cnvimass 6034	. . . . . . . . . . . . . . 15 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
177		fvex 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊‘𝑋) ∈ V
178		snex 5368	. . . . . . . . . . . . . . . . . 18 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ∈ V
179		xpexg 7693	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊‘𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
180	8, 178, 179	sylancl 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V)
181		unexg 7686	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊‘𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∈ V) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
182	177, 180, 181	sylancr 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
183	182	dmexd 7843	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V)
184		ssexg 5251	. . . . . . . . . . . . . . 15 ⊢ (((^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ⊆ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∧ dom ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∈ V) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
185	176, 183, 184	sylancr 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
186	185	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
187		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) → 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}))
188		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
189		simplr 774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
190		nelne2 3032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑋 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
191	188, 189, 190	syl2anc 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)))
192	86, 164	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
193	192	necon3ai 2959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ≠ (𝑋𝐹(𝑊‘𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦)
194		biorf 942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
195	191, 193, 194	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧(𝑊‘𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦)))
196		orcom 876	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ (𝑧(𝑊‘𝑋)𝑦 ∨ 𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦))
197	196, 83	bitr4i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})𝑦 ∨ 𝑧(𝑊‘𝑋)𝑦) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
198	195, 197	bitr2di 289	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦 ↔ 𝑧(𝑊‘𝑋)𝑦))
199		vex 3435	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
200	199	eliniseg 6046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦))
201	200	elv 3436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))𝑦)
202	199	eliniseg 6046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ V → (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦))
203	202	elv 3436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦}) ↔ 𝑧(𝑊‘𝑋)𝑦)
204	198, 201, 203	3bitr4g 315	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ (^◡(𝑊‘𝑋) “ {𝑦})))
205	204	eqrdv 2737	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = (^◡(𝑊‘𝑋) “ {𝑦}))
206	187, 205	sylan9eqr 2796	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = (^◡(𝑊‘𝑋) “ {𝑦}))
207	206	sqxpeqd 5650	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
208	207	ineq2d 4149	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
209		indir 4214	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
210		inxp 5774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})))
211		incom 4138	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))})
212		cnvimass 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ dom (𝑊‘𝑋)
213	18	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
214		dmss 5844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
216		dmxpid 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ dom (𝑋 × 𝑋) = 𝑋
217	215, 216	sseqtrdi 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → dom (𝑊‘𝑋) ⊆ 𝑋)
218	212, 217	sstrid 3926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) ⊆ 𝑋)
219	218, 189	ssneldd 3918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
220		disjsn 4643	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ (^◡(𝑊‘𝑋) “ {𝑦}))
221	219, 220	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
222	211, 221	eqtrid 2786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦})) = ∅)
223	222	xpeq2d 5648	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅))
224		xp0 5718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ∅) = ∅
225	223, 224	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊‘𝑋))} ∩ (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
226	210, 225	eqtrid 2786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ∅)
227	226	uneq2d 4098	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
228	209, 227	eqtrid 2786	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅))
229		un0 4322	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))
230	228, 229	eqtrdi 2790	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
231	230	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
232	208, 231	eqtrd 2774	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦}))))
233	206, 232	oveq12d 7374	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))))
234	233	eqeq1d 2741	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
235	186, 234	sbcied 3766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((^◡(𝑊‘𝑋) “ {𝑦})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑦}) × (^◡(𝑊‘𝑋) “ {𝑦})))) = 𝑦))
236	175, 235	mpbird 258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
237	164	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → 𝑦 = (𝑋𝐹(𝑊‘𝑋)))
238	237	eqcomd 2745	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋𝐹(𝑊‘𝑋)) = 𝑦)
239	185	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) ∈ V)
240		simplr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
241	237	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋)))
242	18	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
243		rnss 5881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
244	242, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ran (𝑊‘𝑋) ⊆ ran (𝑋 × 𝑋))
245		df-rn 5629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑊‘𝑋) = dom ^◡(𝑊‘𝑋)
246		rnxpid 6124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran (𝑋 × 𝑋) = 𝑋
247	244, 245, 246	3sstr3g 3967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → dom ^◡(𝑊‘𝑋) ⊆ 𝑋)
248	247	sseld 3914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋𝐹(𝑊‘𝑋)) ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
249	241, 248	sylbid 241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑦 ∈ dom ^◡(𝑊‘𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
250	240, 249	mtod 199	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋))
251		ndmima 6055	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ dom ^◡(𝑊‘𝑋) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
252	250, 251	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑊‘𝑋) “ {𝑦}) = ∅)
253	237	sneqd 4567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊‘𝑋))})
254	253	imaeq2d 6012	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}))
255		df-ima 5631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))})
256		cnvxp 6108	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
257	256	reseq1i 5927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))})
258		ssid 3937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))}
259		xpssres 5970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ⊆ {(𝑋𝐹(𝑊‘𝑋))} → (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋))
260	258, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
261	257, 260	eqtri 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
262	261	rneqi 5879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋)
263	46	snnz 4708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {(𝑋𝐹(𝑊‘𝑋))} ≠ ∅
264		rnxp 6121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋)
265	263, 264	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran ({(𝑋𝐹(𝑊‘𝑋))} × 𝑋) = 𝑋
266	262, 265	eqtri 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ↾ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
267	255, 266	eqtri 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {(𝑋𝐹(𝑊‘𝑋))}) = 𝑋
268	254, 267	eqtrdi 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}) = 𝑋)
269	252, 268	uneq12d 4099	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
270		cnvun 6093	. . . . . . . . . . . . . . . . . . 19 ⊢ ^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) = (^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}))
271	270	imaeq1i 6009	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})
272		imaundir 6101	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡(𝑊‘𝑋) ∪ ^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
273	271, 272	eqtri 2762	. . . . . . . . . . . . . . . . 17 ⊢ (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = ((^◡(𝑊‘𝑋) “ {𝑦}) ∪ (^◡(𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) “ {𝑦}))
274		un0 4322	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = 𝑋
275		uncom 4088	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
276	274, 275	eqtr3i 2764	. . . . . . . . . . . . . . . . 17 ⊢ 𝑋 = (∅ ∪ 𝑋)
277	269, 273, 276	3eqtr4g 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) = 𝑋)
278	187, 277	sylan9eqr 2796	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
279	278	sqxpeqd 5650	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
280	279	ineq2d 4149	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)))
281		indir 4214	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)))
282		dfss2 3901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
283	242, 282	sylib 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
284		incom 4138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))})
285		disjsn 4643	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
286	240, 285	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊‘𝑋))}) = ∅)
287	284, 286	eqtrid 2786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋) = ∅)
288	287	xpeq2d 5648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
289		xpindi 5775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ({(𝑋𝐹(𝑊‘𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))
290		xp0 5718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 × ∅) = ∅
291	288, 289, 290	3eqtr3g 2797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
292	283, 291	uneq12d 4099	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊‘𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊‘𝑋) ∪ ∅))
293	281, 292	eqtrid 2786	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊‘𝑋) ∪ ∅))
294		un0 4322	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊‘𝑋) ∪ ∅) = (𝑊‘𝑋)
295	293, 294	eqtrdi 2790	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
296	295	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊‘𝑋))
297	280, 296	eqtrd 2774	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊‘𝑋))
298	278, 297	oveq12d 7374	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊‘𝑋)))
299	298	eqeq1d 2741	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) ∧ 𝑢 = (^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
300	239, 299	sbcied 3766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → ([(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊‘𝑋)) = 𝑦))
301	238, 300	mpbird 258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))}) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
302	236, 301	jaodan 965	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
303	134, 302	sylan2b 600	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})) → [(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
304	303	ralrimiva 3131	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
305	173, 304	jca 516	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
306	2, 3	fpwwe2lem2 10546	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
307	306	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝐴 ∧ ((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}))) ∧ (((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})[(^◡((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
308	34, 305, 307	mpbir2and 719	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})))
309	2	relopabiv 5763	. . . . . . 7 ⊢ Rel 𝑊
310	309	releldmi 5890	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))})𝑊((𝑊‘𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊‘𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊)
311		elssuni 4869	. . . . . 6 ⊢ ((𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
312	308, 310, 311	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ ∪ dom 𝑊)
313	312, 7	sseqtrrdi 3956	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊‘𝑋))}) ⊆ 𝑋)
314	1, 313	sstrid 3926	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
315	46	snss 4716	. . 3 ⊢ ((𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊‘𝑋))} ⊆ 𝑋)
316	314, 315	sylibr 235	. 2 ⊢ ((𝜑 ∧ ¬ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
317	316	pm2.18da 805	1 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 ∨ w3o 1091 ∧ w3a 1092 ∀wal 1545 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 Vcvv 3431 [wsbc 3723 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4261 𝒫 cpw 4529 {csn 4555 ∪ cuni 4838 class class class wbr 5072 {copab 5134 Or wor 5525 Fr wfr 5568 We wwe 5570 × cxp 5616 ^◡ccnv 5617 dom cdm 5618 ran crn 5619 ↾ cres 5620 “ cima 5621 Fun wfun 6479 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-oi 9415

This theorem is referenced by: fpwwe2 10557

W3C validator