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

Theorem fpwwe2lem13 9648
Description: Lemma for fpwwe2 9649. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2 (𝜑𝐴 ∈ V)
fpwwe2.3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2.4 𝑋 = dom 𝑊
Assertion
Ref Expression
fpwwe2lem13 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)

Proof of Theorem fpwwe2lem13
Dummy variables 𝑎 𝑏 𝑠 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssun2 3912 . . . 4 {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
2 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
43adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝐴 ∈ V)
5 fpwwe2.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
65adantlr 753 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7 fpwwe2.4 . . . . . . . . . . . . . 14 𝑋 = dom 𝑊
82, 4, 6, 7fpwwe2lem12 9647 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
92, 4, 6, 7fpwwe2lem11 9646 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10 ffun 6201 . . . . . . . . . . . . . 14 (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11 funfvbrb 6485 . . . . . . . . . . . . . 14 (Fun 𝑊 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
129, 10, 113syl 18 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
138, 12mpbid 222 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊𝑋))
142, 4fpwwe2lem2 9638 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊𝑋) ↔ ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
1513, 14mpbid 222 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
1615simpld 477 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)))
1716simpld 477 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝐴)
1816simprd 482 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
1915simprd 482 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
2019simpld 477 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) We 𝑋)
2117, 18, 203jca 1122 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋))
222, 3, 5fpwwe2lem5 9640 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2321, 22syldan 488 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2423snssd 4477 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝐴)
2517, 24unssd 3924 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴)
26 ssun1 3911 . . . . . . . . . . 11 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
27 xpss12 5273 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
2826, 26, 27mp2an 710 . . . . . . . . . 10 (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
2918, 28syl6ss 3748 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
30 xpss12 5273 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3126, 1, 30mp2an 710 . . . . . . . . . 10 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
3231a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3329, 32unssd 3924 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3425, 33jca 555 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))))
35 ssdif0 4077 . . . . . . . . . . . . . 14 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅)
36 simpllr 817 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
3718ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
3837ssbrd 4839 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋))))
39 brxp 5296 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4039simplbi 478 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4138, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4236, 41mtod 189 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)))
43 brxp 5296 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ {(𝑋𝐹(𝑊𝑋))}))
4443simplbi 478 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4536, 44nsyl 135 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))
46 ovex 6833 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐹(𝑊𝑋)) ∈ V
47 breq2 4800 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋))))
48 brun 4847 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
4947, 48syl6bb 276 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5049notbid 307 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑋𝐹(𝑊𝑋)) → (¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5146, 50rexsn 4359 . . . . . . . . . . . . . . . . . 18 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
52 ioran 512 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5351, 52bitri 264 . . . . . . . . . . . . . . . . 17 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5442, 45, 53sylanbrc 701 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
55 simplrr 820 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ≠ ∅)
5655neneqd 2929 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑥 = ∅)
57 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))})
58 sssn 4495 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
5957, 58sylib 208 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
6059ord 391 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (¬ 𝑥 = ∅ → 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
6156, 60mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊𝑋))})
6261raleqdv 3275 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
63 breq1 4799 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6463notbid 307 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6546, 64ralsn 4358 . . . . . . . . . . . . . . . . . 18 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6662, 65syl6bb 276 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6761, 66rexeqbidv 3284 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6854, 67mpbird 247 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6968ex 449 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
7035, 69syl5bir 233 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
71 vex 3335 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
72 difexg 4952 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
7371, 72mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
74 wefr 5248 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Fr 𝑋)
7520, 74syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Fr 𝑋)
7675ad2antrr 764 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑊𝑋) Fr 𝑋)
77 simplrl 819 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
78 uncom 3892 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋)
7977, 78syl6sseq 3784 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋))
80 ssundif 4188 . . . . . . . . . . . . . . . . 17 (𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
8179, 80sylib 208 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
82 simpr 479 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)
83 fri 5220 . . . . . . . . . . . . . . . 16 ((((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
8473, 76, 81, 82, 83syl22anc 1474 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
85 brun 4847 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
86 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑊𝑋)𝑦𝑧(𝑊𝑋)𝑦))
87 brxp 5296 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑧𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
8887simprbi 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
89 eldifn 3868 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9089adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9190pm2.21d 118 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑧(𝑊𝑋)𝑦))
9288, 91syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦))
9386, 92jaod 394 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) → 𝑧(𝑊𝑋)𝑦))
9485, 93syl5bi 232 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
9594con3d 148 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (¬ 𝑧(𝑊𝑋)𝑦 → ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
9695ralimdv 3093 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
97 simpr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9897ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9918ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
10099ssbrd 4839 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦))
101 brxp 5296 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦𝑋))
102101simplbi 478 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
103100, 102syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
10498, 103mtod 189 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦)
105 brxp 5296 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
106105simprbi 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
10790, 106nsyl 135 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
108 brun 4847 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
10963, 108syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
110109notbid 307 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
11146, 110ralsn 4358 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
112 ioran 512 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
113111, 112bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
114104, 107, 113sylanbrc 701 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
11596, 114jctird 568 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
116 ssun1 3911 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
117 undif1 4179 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
118116, 117sseqtr4i 3771 . . . . . . . . . . . . . . . . . . . 20 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))})
119 ralun 3930 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
120 ssralv 3799 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
121118, 119, 120mpsyl 68 . . . . . . . . . . . . . . . . . . 19 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
122115, 121syl6 35 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
123 eldifi 3867 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → 𝑦𝑥)
124123adantl 473 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → 𝑦𝑥)
125122, 124jctild 567 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
126125expimpd 630 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦) → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
127126reximdv2 3144 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
12884, 127mpd 15 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
129128ex 449 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
13070, 129pm2.61dne 3010 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
131130ex 449 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
132131alrimiv 1996 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
133 df-fr 5217 . . . . . . . . . 10 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
134132, 133sylibr 224 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
135 elun 3888 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
136 elun 3888 . . . . . . . . . . . 12 (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
137135, 136anbi12i 735 . . . . . . . . . . 11 ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) ↔ ((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})))
138 weso 5249 . . . . . . . . . . . . . . . 16 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Or 𝑋)
13920, 138syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Or 𝑋)
140 solin 5202 . . . . . . . . . . . . . . 15 (((𝑊𝑋) Or 𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
141139, 140sylan 489 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
142 ssun1 3911 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
143142a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
144143ssbrd 4839 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
145 idd 24 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑦𝑥 = 𝑦))
146143ssbrd 4839 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑦(𝑊𝑋)𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
147144, 145, 1463orim123d 1548 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
148141, 147mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
149148ex 449 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
150 simpr 479 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋))
151150ancomd 466 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
152 brxp 5296 . . . . . . . . . . . . . . 15 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥 ↔ (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
153151, 152sylibr 224 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥)
154 ssun2 3912 . . . . . . . . . . . . . . 15 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
155154ssbri 4841 . . . . . . . . . . . . . 14 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)
156 3mix3 1414 . . . . . . . . . . . . . 14 (𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
157153, 155, 1563syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
158157ex 449 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
159 simpr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
160 brxp 5296 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
161159, 160sylibr 224 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
162154ssbri 4841 . . . . . . . . . . . . . 14 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
163 3mix1 1412 . . . . . . . . . . . . . 14 (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
164161, 162, 1633syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
165164ex 449 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
166 elsni 4330 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑥 = (𝑋𝐹(𝑊𝑋)))
167 elsni 4330 . . . . . . . . . . . . . . 15 (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑦 = (𝑋𝐹(𝑊𝑋)))
168 eqtr3 2773 . . . . . . . . . . . . . . 15 ((𝑥 = (𝑋𝐹(𝑊𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊𝑋))) → 𝑥 = 𝑦)
169166, 167, 168syl2an 495 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = 𝑦)
1701693mix2d 1419 . . . . . . . . . . . . 13 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
171170a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
172149, 158, 165, 171ccased 1025 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
173137, 172syl5bi 232 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
174173ralrimivv 3100 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
175 dfwe2 7138 . . . . . . . . 9 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
176134, 174, 175sylanbrc 701 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
1772fpwwe2cbv 9636 . . . . . . . . . . . . 13 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
178177, 4, 13fpwwe2lem3 9639 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦)
179 cnvimass 5635 . . . . . . . . . . . . . . 15 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
180 fvex 6354 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ∈ V
181 snex 5049 . . . . . . . . . . . . . . . . . 18 {(𝑋𝐹(𝑊𝑋))} ∈ V
182 xpexg 7117 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
1838, 181, 182sylancl 697 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
184 unexg 7116 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
185180, 183, 184sylancr 698 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
186 dmexg 7254 . . . . . . . . . . . . . . . 16 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
187185, 186syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
188 ssexg 4948 . . . . . . . . . . . . . . 15 (((((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∧ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
189179, 187, 188sylancr 698 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
190189adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
191 id 22 . . . . . . . . . . . . . . . 16 (𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) → 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}))
192 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦𝑋)
193 simplr 809 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
194 nelne2 3021 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑋 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
195192, 193, 194syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
19688, 167syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 = (𝑋𝐹(𝑊𝑋)))
197196necon3ai 2949 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ≠ (𝑋𝐹(𝑊𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
198 biorf 419 . . . . . . . . . . . . . . . . . . . 20 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
199195, 197, 1983syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
200 orcom 401 . . . . . . . . . . . . . . . . . . . 20 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
201200, 85bitr4i 267 . . . . . . . . . . . . . . . . . . 19 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
202199, 201syl6rbb 277 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
203 vex 3335 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
204 vex 3335 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
205204eliniseg 5644 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
206203, 205ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
207204eliniseg 5644 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦))
208203, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦)
209202, 206, 2083bitr4g 303 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ ((𝑊𝑋) “ {𝑦})))
210209eqrdv 2750 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = ((𝑊𝑋) “ {𝑦}))
211191, 210sylan9eqr 2808 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = ((𝑊𝑋) “ {𝑦}))
212211sqxpeqd 5290 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
213212ineq2d 3949 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
214 indir 4010 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
215 inxp 5402 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})))
216 incom 3940 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))})
217 cnvimass 5635 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑊𝑋) “ {𝑦}) ⊆ dom (𝑊𝑋)
21818adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
219 dmss 5470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
220218, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
221 dmxpid 5492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑋 × 𝑋) = 𝑋
222220, 221syl6sseq 3784 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ 𝑋)
223217, 222syl5ss 3747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑊𝑋) “ {𝑦}) ⊆ 𝑋)
224223, 193ssneldd 3739 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
225 disjsn 4382 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
226224, 225sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
227216, 226syl5eq 2798 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = ∅)
228227xpeq2d 5288 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅))
229 xp0 5702 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅) = ∅
230228, 229syl6eq 2802 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ∅)
231215, 230syl5eq 2798 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ∅)
232231uneq2d 3902 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
233214, 232syl5eq 2798 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
234 un0 4102 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
235233, 234syl6eq 2802 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
236235adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
237213, 236eqtrd 2786 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
238211, 237oveq12d 6823 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))))
239238eqeq1d 2754 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
240190, 239sbcied 3605 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
241178, 240mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
242167adantl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑦 = (𝑋𝐹(𝑊𝑋)))
243242eqcomd 2758 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋𝐹(𝑊𝑋)) = 𝑦)
244189adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
245 simplr 809 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
246242eleq1d 2816 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) ↔ (𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋)))
24718adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
248 rnss 5501 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
249247, 248syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
250 df-rn 5269 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑊𝑋) = dom (𝑊𝑋)
251 rnxpid 5717 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × 𝑋) = 𝑋
252249, 250, 2513sstr3g 3778 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → dom (𝑊𝑋) ⊆ 𝑋)
253252sseld 3735 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
254246, 253sylbid 230 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
255245, 254mtod 189 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ dom (𝑊𝑋))
256 ndmima 5652 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ dom (𝑊𝑋) → ((𝑊𝑋) “ {𝑦}) = ∅)
257255, 256syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) “ {𝑦}) = ∅)
258242sneqd 4325 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊𝑋))})
259258imaeq2d 5616 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}))
260 df-ima 5271 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))})
261 cnvxp 5701 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
262261reseq1i 5539 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))})
263 ssid 3757 . . . . . . . . . . . . . . . . . . . . . . . 24 {(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))}
264 xpssres 5584 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))} → (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋))
265263, 264ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
266262, 265eqtri 2774 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
267266rneqi 5499 . . . . . . . . . . . . . . . . . . . . 21 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
26846snnz 4444 . . . . . . . . . . . . . . . . . . . . . 22 {(𝑋𝐹(𝑊𝑋))} ≠ ∅
269 rnxp 5714 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑋𝐹(𝑊𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋)
270268, 269ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋
271267, 270eqtri 2774 . . . . . . . . . . . . . . . . . . . 20 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
272260, 271eqtri 2774 . . . . . . . . . . . . . . . . . . 19 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
273259, 272syl6eq 2802 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = 𝑋)
274257, 273uneq12d 3903 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
275 cnvun 5688 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) = ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
276275imaeq1i 5613 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})
277 imaundir 5696 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
278276, 277eqtri 2774 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
279 un0 4102 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = 𝑋
280 uncom 3892 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
281279, 280eqtr3i 2776 . . . . . . . . . . . . . . . . 17 𝑋 = (∅ ∪ 𝑋)
282274, 278, 2813eqtr4g 2811 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = 𝑋)
283191, 282sylan9eqr 2808 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
284283sqxpeqd 5290 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
285284ineq2d 3949 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)))
286 indir 4010 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)))
287 df-ss 3721 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
288247, 287sylib 208 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
289 incom 3940 . . . . . . . . . . . . . . . . . . . . . . 23 ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))})
290 disjsn 4382 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
291245, 290sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
292289, 291syl5eq 2798 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = ∅)
293292xpeq2d 5288 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
294 xpindi 5403 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))
295 xp0 5702 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ∅) = ∅
296293, 294, 2953eqtr3g 2809 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
297288, 296uneq12d 3903 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊𝑋) ∪ ∅))
298286, 297syl5eq 2798 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊𝑋) ∪ ∅))
299 un0 4102 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) ∪ ∅) = (𝑊𝑋)
300298, 299syl6eq 2802 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
301300adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
302285, 301eqtrd 2786 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊𝑋))
303283, 302oveq12d 6823 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊𝑋)))
304303eqeq1d 2754 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
305244, 304sbcied 3605 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
306243, 305mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307241, 306jaodan 861 . . . . . . . . . 10 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
308136, 307sylan2b 493 . . . . . . . . 9 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
309308ralrimiva 3096 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
310176, 309jca 555 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
3112, 3fpwwe2lem2 9638 . . . . . . . 8 (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
312311adantr 472 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
31334, 310, 312mpbir2and 995 . . . . . 6 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
3142relopabi 5393 . . . . . . 7 Rel 𝑊
315314releldmi 5509 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊)
316 elssuni 4611 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
317313, 315, 3163syl 18 . . . . 5 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
318317, 7syl6sseqr 3785 . . . 4 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
3191, 318syl5ss 3747 . . 3 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
32046snss 4452 . . 3 ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
321319, 320sylibr 224 . 2 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
322321pm2.18da 458 1 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3o 1071  w3a 1072  wal 1622   = wceq 1624  wcel 2131  wne 2924  wral 3042  wrex 3043  Vcvv 3332  [wsbc 3568  cdif 3704  cun 3705  cin 3706  wss 3707  c0 4050  𝒫 cpw 4294  {csn 4313   cuni 4580   class class class wbr 4796  {copab 4856   Or wor 5178   Fr wfr 5214   We wwe 5216   × cxp 5256  ccnv 5257  dom cdm 5258  ran crn 5259  cres 5260  cima 5261  Fun wfun 6035  wf 6037  cfv 6041  (class class class)co 6805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-wrecs 7568  df-recs 7629  df-oi 8572
This theorem is referenced by:  fpwwe2  9649
  Copyright terms: Public domain W3C validator