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

Theorem fpwwe2lem13 9719
Description: Lemma for fpwwe2 9720. (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 3941 . . . 4 {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
2 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
43adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝐴 ∈ V)
5 fpwwe2.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
65adantlr 706 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7 fpwwe2.4 . . . . . . . . . . . . . 14 𝑋 = dom 𝑊
82, 4, 6, 7fpwwe2lem12 9718 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
92, 4, 6, 7fpwwe2lem11 9717 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10 ffun 6228 . . . . . . . . . . . . . 14 (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11 funfvbrb 6522 . . . . . . . . . . . . . 14 (Fun 𝑊 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
129, 10, 113syl 18 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
138, 12mpbid 223 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊𝑋))
142, 4fpwwe2lem2 9709 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊𝑋) ↔ ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
1513, 14mpbid 223 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
1615simpld 488 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)))
1716simpld 488 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝐴)
1816simprd 489 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
1915simprd 489 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
2019simpld 488 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) We 𝑋)
2117, 18, 203jca 1158 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋))
222, 3, 5fpwwe2lem5 9711 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2321, 22syldan 585 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2423snssd 4496 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝐴)
2517, 24unssd 3953 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴)
26 ssun1 3940 . . . . . . . . . . 11 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
27 xpss12 5294 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
2826, 26, 27mp2an 683 . . . . . . . . . 10 (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
2918, 28syl6ss 3775 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
30 xpss12 5294 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3126, 1, 30mp2an 683 . . . . . . . . . 10 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
3231a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3329, 32unssd 3953 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3425, 33jca 507 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))))
35 ssdif0 4108 . . . . . . . . . . . . . 14 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅)
36 simpllr 793 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
3718ad2antrr 717 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
3837ssbrd 4854 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋))))
39 brxp 5325 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4039simplbi 491 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4138, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4236, 41mtod 189 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)))
43 brxp 5325 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ {(𝑋𝐹(𝑊𝑋))}))
4443simplbi 491 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4536, 44nsyl 137 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))
46 ovex 6876 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐹(𝑊𝑋)) ∈ V
47 breq2 4815 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋))))
48 brun 4862 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
4947, 48syl6bb 278 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5049notbid 309 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑋𝐹(𝑊𝑋)) → (¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5146, 50rexsn 4382 . . . . . . . . . . . . . . . . . 18 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
52 ioran 1006 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5351, 52bitri 266 . . . . . . . . . . . . . . . . 17 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5442, 45, 53sylanbrc 578 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
55 simplrr 796 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ≠ ∅)
5655neneqd 2942 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑥 = ∅)
57 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))})
58 sssn 4513 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
5957, 58sylib 209 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
6059ord 890 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (¬ 𝑥 = ∅ → 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
6156, 60mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊𝑋))})
6261raleqdv 3292 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
63 breq1 4814 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6463notbid 309 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6546, 64ralsn 4381 . . . . . . . . . . . . . . . . . 18 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6662, 65syl6bb 278 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6761, 66rexeqbidv 3301 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6854, 67mpbird 248 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6968ex 401 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
7035, 69syl5bir 234 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
71 vex 3353 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
72 difexg 4971 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
7371, 72mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
74 wefr 5269 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Fr 𝑋)
7520, 74syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Fr 𝑋)
7675ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑊𝑋) Fr 𝑋)
77 simplrl 795 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
78 uncom 3921 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋)
7977, 78syl6sseq 3813 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋))
80 ssundif 4214 . . . . . . . . . . . . . . . . 17 (𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
8179, 80sylib 209 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
82 simpr 477 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)
83 fri 5241 . . . . . . . . . . . . . . . 16 ((((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
8473, 76, 81, 82, 83syl22anc 867 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
85 brun 4862 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
86 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑊𝑋)𝑦𝑧(𝑊𝑋)𝑦))
87 brxp 5325 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑧𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
8887simprbi 490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
89 eldifn 3897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9089adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9190pm2.21d 119 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑧(𝑊𝑋)𝑦))
9288, 91syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦))
9386, 92jaod 885 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) → 𝑧(𝑊𝑋)𝑦))
9485, 93syl5bi 233 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
9594con3d 149 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (¬ 𝑧(𝑊𝑋)𝑦 → ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
9695ralimdv 3110 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
97 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9897ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9918ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
10099ssbrd 4854 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦))
101 brxp 5325 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦𝑋))
102101simplbi 491 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
103100, 102syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
10498, 103mtod 189 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦)
105 brxp 5325 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
106105simprbi 490 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
10790, 106nsyl 137 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
108 brun 4862 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
10963, 108syl6bb 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
110109notbid 309 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
11146, 110ralsn 4381 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
112 ioran 1006 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
113111, 112bitri 266 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
114104, 107, 113sylanbrc 578 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
11596, 114jctird 522 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
116 ssun1 3940 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
117 undif1 4205 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
118116, 117sseqtr4i 3800 . . . . . . . . . . . . . . . . . . . 20 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))})
119 ralun 3959 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
120 ssralv 3828 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
121118, 119, 120mpsyl 68 . . . . . . . . . . . . . . . . . . 19 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
122115, 121syl6 35 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
123 eldifi 3896 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → 𝑦𝑥)
124123adantl 473 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → 𝑦𝑥)
125122, 124jctild 521 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
126125expimpd 445 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦) → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
127126reximdv2 3160 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
12884, 127mpd 15 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
129128ex 401 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
13070, 129pm2.61dne 3023 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
131130ex 401 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
132131alrimiv 2022 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
133 df-fr 5238 . . . . . . . . . 10 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
134132, 133sylibr 225 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
135 elun 3917 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
136 elun 3917 . . . . . . . . . . . 12 (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
137135, 136anbi12i 620 . . . . . . . . . . 11 ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) ↔ ((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})))
138 weso 5270 . . . . . . . . . . . . . . . 16 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Or 𝑋)
13920, 138syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Or 𝑋)
140 solin 5223 . . . . . . . . . . . . . . 15 (((𝑊𝑋) Or 𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
141139, 140sylan 575 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
142 ssun1 3940 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
143142a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
144143ssbrd 4854 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
145 idd 24 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑦𝑥 = 𝑦))
146143ssbrd 4854 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑦(𝑊𝑋)𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
147144, 145, 1463orim123d 1568 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
148141, 147mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
149148ex 401 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
150 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋))
151150ancomd 453 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
152 brxp 5325 . . . . . . . . . . . . . . 15 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥 ↔ (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
153151, 152sylibr 225 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥)
154 ssun2 3941 . . . . . . . . . . . . . . 15 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
155154ssbri 4856 . . . . . . . . . . . . . 14 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)
156 3mix3 1431 . . . . . . . . . . . . . 14 (𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
157153, 155, 1563syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
158157ex 401 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
159 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
160 brxp 5325 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
161159, 160sylibr 225 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
162154ssbri 4856 . . . . . . . . . . . . . 14 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
163 3mix1 1429 . . . . . . . . . . . . . 14 (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
164161, 162, 1633syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
165164ex 401 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
166 elsni 4353 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑥 = (𝑋𝐹(𝑊𝑋)))
167 elsni 4353 . . . . . . . . . . . . . . 15 (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑦 = (𝑋𝐹(𝑊𝑋)))
168 eqtr3 2786 . . . . . . . . . . . . . . 15 ((𝑥 = (𝑋𝐹(𝑊𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊𝑋))) → 𝑥 = 𝑦)
169166, 167, 168syl2an 589 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = 𝑦)
1701693mix2d 1436 . . . . . . . . . . . . 13 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
171170a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
172149, 158, 165, 171ccased 1061 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
173137, 172syl5bi 233 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
174173ralrimivv 3117 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
175 dfwe2 7181 . . . . . . . . 9 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
176134, 174, 175sylanbrc 578 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
1772fpwwe2cbv 9707 . . . . . . . . . . . . 13 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
178177, 4, 13fpwwe2lem3 9710 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦)
179 cnvimass 5669 . . . . . . . . . . . . . . 15 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
180 fvex 6390 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ∈ V
181 snex 5066 . . . . . . . . . . . . . . . . . 18 {(𝑋𝐹(𝑊𝑋))} ∈ V
182 xpexg 7160 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
1838, 181, 182sylancl 580 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
184 unexg 7159 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
185180, 183, 184sylancr 581 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
186 dmexg 7297 . . . . . . . . . . . . . . . 16 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
187185, 186syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
188 ssexg 4967 . . . . . . . . . . . . . . 15 (((((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∧ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
189179, 187, 188sylancr 581 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
190189adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
191 id 22 . . . . . . . . . . . . . . . 16 (𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) → 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}))
192 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦𝑋)
193 simplr 785 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
194 nelne2 3034 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑋 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
195192, 193, 194syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
19688, 167syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 = (𝑋𝐹(𝑊𝑋)))
197196necon3ai 2962 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ≠ (𝑋𝐹(𝑊𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
198 biorf 960 . . . . . . . . . . . . . . . . . . . 20 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
199195, 197, 1983syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
200 orcom 896 . . . . . . . . . . . . . . . . . . . 20 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
201200, 85bitr4i 269 . . . . . . . . . . . . . . . . . . 19 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
202199, 201syl6rbb 279 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
203 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
204 vex 3353 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
205204eliniseg 5678 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
206203, 205ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
207204eliniseg 5678 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦))
208203, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦)
209202, 206, 2083bitr4g 305 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ ((𝑊𝑋) “ {𝑦})))
210209eqrdv 2763 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = ((𝑊𝑋) “ {𝑦}))
211191, 210sylan9eqr 2821 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = ((𝑊𝑋) “ {𝑦}))
212211sqxpeqd 5311 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
213212ineq2d 3978 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
214 indir 4042 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
215 inxp 5425 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})))
216 incom 3969 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))})
217 cnvimass 5669 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑊𝑋) “ {𝑦}) ⊆ dom (𝑊𝑋)
21818adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
219 dmss 5493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
220218, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
221 dmxpid 5515 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑋 × 𝑋) = 𝑋
222220, 221syl6sseq 3813 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ 𝑋)
223217, 222syl5ss 3774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑊𝑋) “ {𝑦}) ⊆ 𝑋)
224223, 193ssneldd 3766 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
225 disjsn 4404 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
226224, 225sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
227216, 226syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = ∅)
228227xpeq2d 5309 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅))
229 xp0 5737 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅) = ∅
230228, 229syl6eq 2815 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ∅)
231215, 230syl5eq 2811 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ∅)
232231uneq2d 3931 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
233214, 232syl5eq 2811 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
234 un0 4131 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
235233, 234syl6eq 2815 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
236235adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
237213, 236eqtrd 2799 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
238211, 237oveq12d 6862 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))))
239238eqeq1d 2767 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
240190, 239sbcied 3635 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
241178, 240mpbird 248 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
242167adantl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑦 = (𝑋𝐹(𝑊𝑋)))
243242eqcomd 2771 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋𝐹(𝑊𝑋)) = 𝑦)
244189adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
245 simplr 785 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
246242eleq1d 2829 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) ↔ (𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋)))
24718adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
248 rnss 5524 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
249247, 248syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
250 df-rn 5290 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑊𝑋) = dom (𝑊𝑋)
251 rnxpid 5752 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × 𝑋) = 𝑋
252249, 250, 2513sstr3g 3807 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → dom (𝑊𝑋) ⊆ 𝑋)
253252sseld 3762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
254246, 253sylbid 231 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
255245, 254mtod 189 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ dom (𝑊𝑋))
256 ndmima 5686 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ dom (𝑊𝑋) → ((𝑊𝑋) “ {𝑦}) = ∅)
257255, 256syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) “ {𝑦}) = ∅)
258242sneqd 4348 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊𝑋))})
259258imaeq2d 5650 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}))
260 df-ima 5292 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))})
261 cnvxp 5736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
262261reseq1i 5563 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))})
263 ssid 3785 . . . . . . . . . . . . . . . . . . . . . . . 24 {(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))}
264 xpssres 5610 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))} → (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋))
265263, 264ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
266262, 265eqtri 2787 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
267266rneqi 5522 . . . . . . . . . . . . . . . . . . . . 21 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
26846snnz 4465 . . . . . . . . . . . . . . . . . . . . . 22 {(𝑋𝐹(𝑊𝑋))} ≠ ∅
269 rnxp 5749 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑋𝐹(𝑊𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋)
270268, 269ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋
271267, 270eqtri 2787 . . . . . . . . . . . . . . . . . . . 20 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
272260, 271eqtri 2787 . . . . . . . . . . . . . . . . . . 19 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
273259, 272syl6eq 2815 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = 𝑋)
274257, 273uneq12d 3932 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
275 cnvun 5723 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) = ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
276275imaeq1i 5647 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})
277 imaundir 5731 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
278276, 277eqtri 2787 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
279 un0 4131 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = 𝑋
280 uncom 3921 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
281279, 280eqtr3i 2789 . . . . . . . . . . . . . . . . 17 𝑋 = (∅ ∪ 𝑋)
282274, 278, 2813eqtr4g 2824 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = 𝑋)
283191, 282sylan9eqr 2821 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
284283sqxpeqd 5311 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
285284ineq2d 3978 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)))
286 indir 4042 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)))
287 df-ss 3748 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
288247, 287sylib 209 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
289 incom 3969 . . . . . . . . . . . . . . . . . . . . . . 23 ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))})
290 disjsn 4404 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
291245, 290sylibr 225 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
292289, 291syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = ∅)
293292xpeq2d 5309 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
294 xpindi 5426 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))
295 xp0 5737 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ∅) = ∅
296293, 294, 2953eqtr3g 2822 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
297288, 296uneq12d 3932 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊𝑋) ∪ ∅))
298286, 297syl5eq 2811 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊𝑋) ∪ ∅))
299 un0 4131 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) ∪ ∅) = (𝑊𝑋)
300298, 299syl6eq 2815 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
301300adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
302285, 301eqtrd 2799 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊𝑋))
303283, 302oveq12d 6862 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊𝑋)))
304303eqeq1d 2767 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
305244, 304sbcied 3635 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
306243, 305mpbird 248 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307241, 306jaodan 980 . . . . . . . . . 10 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
308136, 307sylan2b 587 . . . . . . . . 9 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
309308ralrimiva 3113 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
310176, 309jca 507 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
3112, 3fpwwe2lem2 9709 . . . . . . . 8 (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
312311adantr 472 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
31334, 310, 312mpbir2and 704 . . . . . 6 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
3142relopabi 5416 . . . . . . 7 Rel 𝑊
315314releldmi 5533 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊)
316 elssuni 4627 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
317313, 315, 3163syl 18 . . . . 5 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
318317, 7syl6sseqr 3814 . . . 4 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
3191, 318syl5ss 3774 . . 3 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
32046snss 4472 . . 3 ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
321319, 320sylibr 225 . 2 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
322321pm2.18da 834 1 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3o 1106  w3a 1107  wal 1650   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  [wsbc 3598  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081  𝒫 cpw 4317  {csn 4336   cuni 4596   class class class wbr 4811  {copab 4873   Or wor 5199   Fr wfr 5235   We wwe 5237   × cxp 5277  ccnv 5278  dom cdm 5279  ran crn 5280  cres 5281  cima 5282  Fun wfun 6064  wf 6066  cfv 6070  (class class class)co 6844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-wrecs 7612  df-recs 7674  df-oi 8624
This theorem is referenced by:  fpwwe2  9720
  Copyright terms: Public domain W3C validator