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

Theorem fpwwe2lem13 9408
Description: Lemma for fpwwe2 9409. (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 3755 . . . 4 {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
2 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
43adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝐴 ∈ V)
5 fpwwe2.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
65adantlr 750 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7 fpwwe2.4 . . . . . . . . . . . . . 14 𝑋 = dom 𝑊
82, 4, 6, 7fpwwe2lem12 9407 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
92, 4, 6, 7fpwwe2lem11 9406 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10 ffun 6005 . . . . . . . . . . . . . 14 (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11 funfvbrb 6286 . . . . . . . . . . . . . 14 (Fun 𝑊 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
129, 10, 113syl 18 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
138, 12mpbid 222 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊𝑋))
142, 4fpwwe2lem2 9398 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊𝑋) ↔ ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
1513, 14mpbid 222 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
1615simpld 475 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)))
1716simpld 475 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝐴)
1816simprd 479 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
1915simprd 479 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
2019simpld 475 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) We 𝑋)
2117, 18, 203jca 1240 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋))
222, 3, 5fpwwe2lem5 9400 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2321, 22syldan 487 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2423snssd 4309 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝐴)
2517, 24unssd 3767 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴)
26 ssun1 3754 . . . . . . . . . . 11 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
27 xpss12 5186 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
2826, 26, 27mp2an 707 . . . . . . . . . 10 (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
2918, 28syl6ss 3595 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
30 xpss12 5186 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3126, 1, 30mp2an 707 . . . . . . . . . 10 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
3231a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3329, 32unssd 3767 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3425, 33jca 554 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))))
35 ssdif0 3916 . . . . . . . . . . . . . 14 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅)
36 simpllr 798 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
3718ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
3837ssbrd 4656 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋))))
39 brxp 5107 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4039simplbi 476 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4138, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4236, 41mtod 189 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)))
43 brxp 5107 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ {(𝑋𝐹(𝑊𝑋))}))
4443simplbi 476 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4536, 44nsyl 135 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))
46 ovex 6632 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐹(𝑊𝑋)) ∈ V
47 breq2 4617 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋))))
48 brun 4663 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
4947, 48syl6bb 276 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5049notbid 308 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑋𝐹(𝑊𝑋)) → (¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5146, 50rexsn 4194 . . . . . . . . . . . . . . . . . 18 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
52 ioran 511 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5351, 52bitri 264 . . . . . . . . . . . . . . . . 17 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5442, 45, 53sylanbrc 697 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
55 simplrr 800 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ≠ ∅)
5655neneqd 2795 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑥 = ∅)
57 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))})
58 sssn 4326 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
5957, 58sylib 208 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
6059ord 392 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (¬ 𝑥 = ∅ → 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
6156, 60mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊𝑋))})
6261raleqdv 3133 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
63 breq1 4616 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6463notbid 308 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6546, 64ralsn 4193 . . . . . . . . . . . . . . . . . 18 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6662, 65syl6bb 276 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6761, 66rexeqbidv 3142 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6854, 67mpbird 247 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6968ex 450 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
7035, 69syl5bir 233 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
71 vex 3189 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
72 difexg 4768 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
7371, 72mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
74 wefr 5064 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Fr 𝑋)
7520, 74syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Fr 𝑋)
7675ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑊𝑋) Fr 𝑋)
77 simplrl 799 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
78 uncom 3735 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋)
7977, 78syl6sseq 3630 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋))
80 ssundif 4024 . . . . . . . . . . . . . . . . 17 (𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
8179, 80sylib 208 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
82 simpr 477 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)
83 fri 5036 . . . . . . . . . . . . . . . 16 ((((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
8473, 76, 81, 82, 83syl22anc 1324 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
85 brun 4663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
86 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑊𝑋)𝑦𝑧(𝑊𝑋)𝑦))
87 brxp 5107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑧𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
8887simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
89 eldifn 3711 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9089adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9190pm2.21d 118 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑧(𝑊𝑋)𝑦))
9288, 91syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦))
9386, 92jaod 395 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) → 𝑧(𝑊𝑋)𝑦))
9485, 93syl5bi 232 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
9594con3d 148 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (¬ 𝑧(𝑊𝑋)𝑦 → ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
9695ralimdv 2957 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
97 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9897ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9918ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
10099ssbrd 4656 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦))
101 brxp 5107 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦𝑋))
102101simplbi 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
103100, 102syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
10498, 103mtod 189 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦)
105 brxp 5107 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
106105simprbi 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
10790, 106nsyl 135 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
108 brun 4663 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
10963, 108syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
110109notbid 308 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
11146, 110ralsn 4193 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
112 ioran 511 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
113111, 112bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
114104, 107, 113sylanbrc 697 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
11596, 114jctird 566 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
116 ssun1 3754 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
117 undif1 4015 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
118116, 117sseqtr4i 3617 . . . . . . . . . . . . . . . . . . . 20 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))})
119 ralun 3773 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
120 ssralv 3645 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
121118, 119, 120mpsyl 68 . . . . . . . . . . . . . . . . . . 19 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
122115, 121syl6 35 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
123 eldifi 3710 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → 𝑦𝑥)
124123adantl 482 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → 𝑦𝑥)
125122, 124jctild 565 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
126125expimpd 628 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦) → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
127126reximdv2 3008 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
12884, 127mpd 15 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
129128ex 450 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
13070, 129pm2.61dne 2876 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
131130ex 450 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
132131alrimiv 1852 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
133 df-fr 5033 . . . . . . . . . 10 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
134132, 133sylibr 224 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
135 elun 3731 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
136 elun 3731 . . . . . . . . . . . 12 (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
137135, 136anbi12i 732 . . . . . . . . . . 11 ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) ↔ ((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})))
138 weso 5065 . . . . . . . . . . . . . . . 16 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Or 𝑋)
13920, 138syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Or 𝑋)
140 solin 5018 . . . . . . . . . . . . . . 15 (((𝑊𝑋) Or 𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
141139, 140sylan 488 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
142 ssun1 3754 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
143142a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
144143ssbrd 4656 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
145 idd 24 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑦𝑥 = 𝑦))
146143ssbrd 4656 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑦(𝑊𝑋)𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
147144, 145, 1463orim123d 1404 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
148141, 147mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
149148ex 450 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
150 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋))
151150ancomd 467 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
152 brxp 5107 . . . . . . . . . . . . . . 15 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥 ↔ (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
153151, 152sylibr 224 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥)
154 ssun2 3755 . . . . . . . . . . . . . . 15 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
155154ssbri 4657 . . . . . . . . . . . . . 14 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)
156 3mix3 1230 . . . . . . . . . . . . . 14 (𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
157153, 155, 1563syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
158157ex 450 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
159 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
160 brxp 5107 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
161159, 160sylibr 224 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
162154ssbri 4657 . . . . . . . . . . . . . 14 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
163 3mix1 1228 . . . . . . . . . . . . . 14 (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
164161, 162, 1633syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
165164ex 450 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
166 elsni 4165 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑥 = (𝑋𝐹(𝑊𝑋)))
167 elsni 4165 . . . . . . . . . . . . . . 15 (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑦 = (𝑋𝐹(𝑊𝑋)))
168 eqtr3 2642 . . . . . . . . . . . . . . 15 ((𝑥 = (𝑋𝐹(𝑊𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊𝑋))) → 𝑥 = 𝑦)
169166, 167, 168syl2an 494 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = 𝑦)
1701693mix2d 1235 . . . . . . . . . . . . 13 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
171170a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
172149, 158, 165, 171ccased 987 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
173137, 172syl5bi 232 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
174173ralrimivv 2964 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
175 dfwe2 6928 . . . . . . . . 9 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
176134, 174, 175sylanbrc 697 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
1772fpwwe2cbv 9396 . . . . . . . . . . . . 13 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
178177, 4, 13fpwwe2lem3 9399 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦)
179 cnvimass 5444 . . . . . . . . . . . . . . 15 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
180 fvex 6158 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ∈ V
181 snex 4869 . . . . . . . . . . . . . . . . . 18 {(𝑋𝐹(𝑊𝑋))} ∈ V
182 xpexg 6913 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
1838, 181, 182sylancl 693 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
184 unexg 6912 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
185180, 183, 184sylancr 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
186 dmexg 7044 . . . . . . . . . . . . . . . 16 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
187185, 186syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
188 ssexg 4764 . . . . . . . . . . . . . . 15 (((((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∧ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
189179, 187, 188sylancr 694 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
190189adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
191 id 22 . . . . . . . . . . . . . . . 16 (𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) → 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}))
192 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦𝑋)
193 simplr 791 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
194 nelne2 2887 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑋 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
195192, 193, 194syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
19688, 167syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 = (𝑋𝐹(𝑊𝑋)))
197196necon3ai 2815 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ≠ (𝑋𝐹(𝑊𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
198 biorf 420 . . . . . . . . . . . . . . . . . . . 20 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
199195, 197, 1983syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
200 orcom 402 . . . . . . . . . . . . . . . . . . . 20 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
201200, 85bitr4i 267 . . . . . . . . . . . . . . . . . . 19 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
202199, 201syl6rbb 277 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
203 vex 3189 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
204 vex 3189 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
205204eliniseg 5453 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
206203, 205ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
207204eliniseg 5453 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦))
208203, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦)
209202, 206, 2083bitr4g 303 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ ((𝑊𝑋) “ {𝑦})))
210209eqrdv 2619 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = ((𝑊𝑋) “ {𝑦}))
211191, 210sylan9eqr 2677 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = ((𝑊𝑋) “ {𝑦}))
212211sqxpeqd 5101 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
213212ineq2d 3792 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
214 indir 3851 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
215 inxp 5214 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})))
216 incom 3783 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))})
217 cnvimass 5444 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑊𝑋) “ {𝑦}) ⊆ dom (𝑊𝑋)
21818adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
219 dmss 5283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
220218, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
221 dmxpid 5305 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑋 × 𝑋) = 𝑋
222220, 221syl6sseq 3630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ 𝑋)
223217, 222syl5ss 3594 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑊𝑋) “ {𝑦}) ⊆ 𝑋)
224223, 193ssneldd 3586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
225 disjsn 4216 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
226224, 225sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
227216, 226syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = ∅)
228227xpeq2d 5099 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅))
229 xp0 5511 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅) = ∅
230228, 229syl6eq 2671 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ∅)
231215, 230syl5eq 2667 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ∅)
232231uneq2d 3745 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
233214, 232syl5eq 2667 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
234 un0 3939 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
235233, 234syl6eq 2671 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
236235adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
237213, 236eqtrd 2655 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
238211, 237oveq12d 6622 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))))
239238eqeq1d 2623 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
240190, 239sbcied 3454 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
241178, 240mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
242167adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑦 = (𝑋𝐹(𝑊𝑋)))
243242eqcomd 2627 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋𝐹(𝑊𝑋)) = 𝑦)
244189adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
245 simplr 791 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
246242eleq1d 2683 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) ↔ (𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋)))
24718adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
248 rnss 5314 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
249247, 248syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
250 df-rn 5085 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑊𝑋) = dom (𝑊𝑋)
251 rnxpid 5526 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × 𝑋) = 𝑋
252249, 250, 2513sstr3g 3624 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → dom (𝑊𝑋) ⊆ 𝑋)
253252sseld 3582 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
254246, 253sylbid 230 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
255245, 254mtod 189 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ dom (𝑊𝑋))
256 ndmima 5461 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ dom (𝑊𝑋) → ((𝑊𝑋) “ {𝑦}) = ∅)
257255, 256syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) “ {𝑦}) = ∅)
258242sneqd 4160 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊𝑋))})
259258imaeq2d 5425 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}))
260 df-ima 5087 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))})
261 cnvxp 5510 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
262261reseq1i 5352 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))})
263 ssid 3603 . . . . . . . . . . . . . . . . . . . . . . . 24 {(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))}
264 xpssres 5393 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))} → (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋))
265263, 264ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
266262, 265eqtri 2643 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
267266rneqi 5312 . . . . . . . . . . . . . . . . . . . . 21 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
26846snnz 4279 . . . . . . . . . . . . . . . . . . . . . 22 {(𝑋𝐹(𝑊𝑋))} ≠ ∅
269 rnxp 5523 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑋𝐹(𝑊𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋)
270268, 269ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋
271267, 270eqtri 2643 . . . . . . . . . . . . . . . . . . . 20 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
272260, 271eqtri 2643 . . . . . . . . . . . . . . . . . . 19 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
273259, 272syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = 𝑋)
274257, 273uneq12d 3746 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
275 cnvun 5497 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) = ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
276275imaeq1i 5422 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})
277 imaundir 5505 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
278276, 277eqtri 2643 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
279 un0 3939 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = 𝑋
280 uncom 3735 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
281279, 280eqtr3i 2645 . . . . . . . . . . . . . . . . 17 𝑋 = (∅ ∪ 𝑋)
282274, 278, 2813eqtr4g 2680 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = 𝑋)
283191, 282sylan9eqr 2677 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
284283sqxpeqd 5101 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
285284ineq2d 3792 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)))
286 indir 3851 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)))
287 df-ss 3569 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
288247, 287sylib 208 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
289 incom 3783 . . . . . . . . . . . . . . . . . . . . . . 23 ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))})
290 disjsn 4216 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
291245, 290sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
292289, 291syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = ∅)
293292xpeq2d 5099 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
294 xpindi 5215 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))
295 xp0 5511 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ∅) = ∅
296293, 294, 2953eqtr3g 2678 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
297288, 296uneq12d 3746 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊𝑋) ∪ ∅))
298286, 297syl5eq 2667 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊𝑋) ∪ ∅))
299 un0 3939 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) ∪ ∅) = (𝑊𝑋)
300298, 299syl6eq 2671 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
301300adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
302285, 301eqtrd 2655 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊𝑋))
303283, 302oveq12d 6622 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊𝑋)))
304303eqeq1d 2623 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
305244, 304sbcied 3454 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
306243, 305mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307241, 306jaodan 825 . . . . . . . . . 10 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
308136, 307sylan2b 492 . . . . . . . . 9 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
309308ralrimiva 2960 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
310176, 309jca 554 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
3112, 3fpwwe2lem2 9398 . . . . . . . 8 (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
312311adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
31334, 310, 312mpbir2and 956 . . . . . 6 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
3142relopabi 5205 . . . . . . 7 Rel 𝑊
315314releldmi 5322 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊)
316 elssuni 4433 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
317313, 315, 3163syl 18 . . . . 5 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
318317, 7syl6sseqr 3631 . . . 4 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
3191, 318syl5ss 3594 . . 3 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
32046snss 4286 . . 3 ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
321319, 320sylibr 224 . 2 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
322321pm2.18da 459 1 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1035  w3a 1036  wal 1478   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186  [wsbc 3417  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891  𝒫 cpw 4130  {csn 4148   cuni 4402   class class class wbr 4613  {copab 4672   Or wor 4994   Fr wfr 5030   We wwe 5032   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  Fun wfun 5841  wf 5843  cfv 5847  (class class class)co 6604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-wrecs 7352  df-recs 7413  df-oi 8359
This theorem is referenced by:  fpwwe2  9409
  Copyright terms: Public domain W3C validator