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

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

Proof of Theorem fpwwe2lem12
Dummy variables 𝑎 𝑏 𝑠 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssun2 4188 . . . 4 {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
2 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . . . . . . . 15 (𝜑𝐴𝑉)
43adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝐴𝑉)
5 fpwwe2.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
65adantlr 715 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7 fpwwe2.4 . . . . . . . . . . . . . 14 𝑋 = dom 𝑊
82, 4, 6, 7fpwwe2lem11 10678 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
92, 4, 6, 7fpwwe2lem10 10677 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10 ffun 6739 . . . . . . . . . . . . . 14 (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11 funfvbrb 7070 . . . . . . . . . . . . . 14 (Fun 𝑊 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
129, 10, 113syl 18 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
138, 12mpbid 232 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊𝑋))
142, 4fpwwe2lem2 10669 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊𝑋) ↔ ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
1513, 14mpbid 232 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
1615simpld 494 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)))
1716simpld 494 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝐴)
1816simprd 495 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
1915simprd 495 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
2019simpld 494 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) We 𝑋)
2117, 18, 203jca 1127 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋))
222, 3, 5fpwwe2lem4 10671 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2321, 22syldan 591 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2423snssd 4813 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝐴)
2517, 24unssd 4201 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴)
26 ssun1 4187 . . . . . . . . . . 11 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
27 xpss12 5703 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
2826, 26, 27mp2an 692 . . . . . . . . . 10 (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
2918, 28sstrdi 4007 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
30 xpss12 5703 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3126, 1, 30mp2an 692 . . . . . . . . . 10 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
3231a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3329, 32unssd 4201 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3425, 33jca 511 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))))
35 ssdif0 4371 . . . . . . . . . . . . . 14 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅)
36 simpllr 776 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
3718ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
3837ssbrd 5190 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋))))
39 brxp 5737 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4039simplbi 497 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4138, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4236, 41mtod 198 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)))
43 brxp 5737 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ {(𝑋𝐹(𝑊𝑋))}))
4443simplbi 497 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4536, 44nsyl 140 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))
46 ovex 7463 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐹(𝑊𝑋)) ∈ V
47 breq2 5151 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋))))
48 brun 5198 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
4947, 48bitrdi 287 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5049notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑋𝐹(𝑊𝑋)) → (¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5146, 50rexsn 4686 . . . . . . . . . . . . . . . . . 18 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
52 ioran 985 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5351, 52bitri 275 . . . . . . . . . . . . . . . . 17 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5442, 45, 53sylanbrc 583 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
55 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))})
56 sssn 4830 . . . . . . . . . . . . . . . . . . 19 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
5755, 56sylib 218 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
58 simplrr 778 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ≠ ∅)
5958neneqd 2942 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑥 = ∅)
6057, 59orcnd 878 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊𝑋))})
6160raleqdv 3323 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
62 breq1 5150 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6362notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6446, 63ralsn 4685 . . . . . . . . . . . . . . . . . 18 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6561, 64bitrdi 287 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6660, 65rexeqbidv 3344 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6754, 66mpbird 257 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6867ex 412 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6935, 68biimtrrid 243 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
70 vex 3481 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
71 difexg 5334 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
7270, 71mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
73 wefr 5678 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Fr 𝑋)
7420, 73syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Fr 𝑋)
7574ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑊𝑋) Fr 𝑋)
76 simplrl 777 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
77 uncom 4167 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋)
7876, 77sseqtrdi 4045 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋))
79 ssundif 4493 . . . . . . . . . . . . . . . . 17 (𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
8078, 79sylib 218 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
81 simpr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)
82 fri 5645 . . . . . . . . . . . . . . . 16 ((((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
8372, 75, 80, 81, 82syl22anc 839 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
84 brun 5198 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
85 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑊𝑋)𝑦𝑧(𝑊𝑋)𝑦))
86 brxp 5737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑧𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
8786simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
88 eldifn 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
8988adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9089pm2.21d 121 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑧(𝑊𝑋)𝑦))
9187, 90syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦))
9285, 91jaod 859 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) → 𝑧(𝑊𝑋)𝑦))
9384, 92biimtrid 242 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
9493con3d 152 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (¬ 𝑧(𝑊𝑋)𝑦 → ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
9594ralimdv 3166 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
96 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9796ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9818ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
9998ssbrd 5190 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦))
100 brxp 5737 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦𝑋))
101100simplbi 497 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
10299, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
10397, 102mtod 198 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦)
104 brxp 5737 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
105104simprbi 496 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
10689, 105nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
107 brun 5198 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
10862, 107bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
109108notbid 318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
11046, 109ralsn 4685 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
111 ioran 985 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
112110, 111bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
113103, 106, 112sylanbrc 583 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
11495, 113jctird 526 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
115 ssun1 4187 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
116 undif1 4481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
117115, 116sseqtrri 4032 . . . . . . . . . . . . . . . . . . . 20 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))})
118 ralun 4207 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
119 ssralv 4063 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
120117, 118, 119mpsyl 68 . . . . . . . . . . . . . . . . . . 19 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
121114, 120syl6 35 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
122 eldifi 4140 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → 𝑦𝑥)
123122adantl 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → 𝑦𝑥)
124121, 123jctild 525 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
125124expimpd 453 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦) → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
126125reximdv2 3161 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
12783, 126mpd 15 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
128127ex 412 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
12969, 128pm2.61dne 3025 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
130129ex 412 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
131130alrimiv 1924 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
132 df-fr 5640 . . . . . . . . . 10 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
133131, 132sylibr 234 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
134 elun 4162 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
135 elun 4162 . . . . . . . . . . . 12 (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
136134, 135anbi12i 628 . . . . . . . . . . 11 ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) ↔ ((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})))
137 weso 5679 . . . . . . . . . . . . . . . 16 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Or 𝑋)
13820, 137syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Or 𝑋)
139 solin 5622 . . . . . . . . . . . . . . 15 (((𝑊𝑋) Or 𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
140138, 139sylan 580 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
141 ssun1 4187 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
142141a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
143142ssbrd 5190 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
144 idd 24 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑦𝑥 = 𝑦))
145142ssbrd 5190 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑦(𝑊𝑋)𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
146143, 144, 1453orim123d 1443 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
147140, 146mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
148147ex 412 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
149 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋))
150149ancomd 461 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
151 brxp 5737 . . . . . . . . . . . . . . 15 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥 ↔ (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
152150, 151sylibr 234 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥)
153 ssun2 4188 . . . . . . . . . . . . . . 15 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
154153ssbri 5192 . . . . . . . . . . . . . 14 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)
155 3mix3 1331 . . . . . . . . . . . . . 14 (𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
156152, 154, 1553syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
157156ex 412 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
158 simpr 484 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
159 brxp 5737 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
160158, 159sylibr 234 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
161153ssbri 5192 . . . . . . . . . . . . . 14 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
162 3mix1 1329 . . . . . . . . . . . . . 14 (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
163160, 161, 1623syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
164163ex 412 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
165 elsni 4647 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑥 = (𝑋𝐹(𝑊𝑋)))
166 elsni 4647 . . . . . . . . . . . . . . 15 (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑦 = (𝑋𝐹(𝑊𝑋)))
167 eqtr3 2760 . . . . . . . . . . . . . . 15 ((𝑥 = (𝑋𝐹(𝑊𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊𝑋))) → 𝑥 = 𝑦)
168165, 166, 167syl2an 596 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = 𝑦)
1691683mix2d 1336 . . . . . . . . . . . . 13 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
170169a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
171148, 157, 164, 170ccased 1038 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
172136, 171biimtrid 242 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
173172ralrimivv 3197 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
174 dfwe2 7792 . . . . . . . . 9 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
175133, 173, 174sylanbrc 583 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
1762fpwwe2cbv 10667 . . . . . . . . . . . . 13 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
177176, 4, 13fpwwe2lem3 10670 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦)
178 cnvimass 6101 . . . . . . . . . . . . . . 15 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
179 fvex 6919 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ∈ V
180 snex 5441 . . . . . . . . . . . . . . . . . 18 {(𝑋𝐹(𝑊𝑋))} ∈ V
181 xpexg 7768 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
1828, 180, 181sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
183 unexg 7761 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
184179, 182, 183sylancr 587 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
185184dmexd 7925 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
186 ssexg 5328 . . . . . . . . . . . . . . 15 (((((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∧ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
187178, 185, 186sylancr 587 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
188187adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
189 id 22 . . . . . . . . . . . . . . . 16 (𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) → 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}))
190 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦𝑋)
191 simplr 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
192 nelne2 3037 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑋 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
193190, 191, 192syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
19487, 166syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 = (𝑋𝐹(𝑊𝑋)))
195194necon3ai 2962 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ≠ (𝑋𝐹(𝑊𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
196 biorf 936 . . . . . . . . . . . . . . . . . . . 20 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
197193, 195, 1963syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
198 orcom 870 . . . . . . . . . . . . . . . . . . . 20 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
199198, 84bitr4i 278 . . . . . . . . . . . . . . . . . . 19 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
200197, 199bitr2di 288 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
201 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
202201eliniseg 6114 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
203202elv 3482 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
204201eliniseg 6114 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦))
205204elv 3482 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦)
206200, 203, 2053bitr4g 314 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ ((𝑊𝑋) “ {𝑦})))
207206eqrdv 2732 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = ((𝑊𝑋) “ {𝑦}))
208189, 207sylan9eqr 2796 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = ((𝑊𝑋) “ {𝑦}))
209208sqxpeqd 5720 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
210209ineq2d 4227 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
211 indir 4291 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
212 inxp 5844 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})))
213 incom 4216 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))})
214 cnvimass 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑊𝑋) “ {𝑦}) ⊆ dom (𝑊𝑋)
21518adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
216 dmss 5915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
217215, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
218 dmxpid 5943 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑋 × 𝑋) = 𝑋
219217, 218sseqtrdi 4045 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ 𝑋)
220214, 219sstrid 4006 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑊𝑋) “ {𝑦}) ⊆ 𝑋)
221220, 191ssneldd 3997 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
222 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
223221, 222sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
224213, 223eqtrid 2786 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = ∅)
225224xpeq2d 5718 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅))
226 xp0 6179 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅) = ∅
227225, 226eqtrdi 2790 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ∅)
228212, 227eqtrid 2786 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ∅)
229228uneq2d 4177 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
230211, 229eqtrid 2786 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
231 un0 4399 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
232230, 231eqtrdi 2790 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
233232adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
234210, 233eqtrd 2774 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
235208, 234oveq12d 7448 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))))
236235eqeq1d 2736 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
237188, 236sbcied 3836 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
238177, 237mpbird 257 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
239166adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑦 = (𝑋𝐹(𝑊𝑋)))
240239eqcomd 2740 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋𝐹(𝑊𝑋)) = 𝑦)
241187adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
242 simplr 769 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
243239eleq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) ↔ (𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋)))
24418adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
245 rnss 5952 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
247 df-rn 5699 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑊𝑋) = dom (𝑊𝑋)
248 rnxpid 6194 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × 𝑋) = 𝑋
249246, 247, 2483sstr3g 4039 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → dom (𝑊𝑋) ⊆ 𝑋)
250249sseld 3993 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
251243, 250sylbid 240 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
252242, 251mtod 198 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ dom (𝑊𝑋))
253 ndmima 6123 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ dom (𝑊𝑋) → ((𝑊𝑋) “ {𝑦}) = ∅)
254252, 253syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) “ {𝑦}) = ∅)
255239sneqd 4642 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊𝑋))})
256255imaeq2d 6079 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}))
257 df-ima 5701 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))})
258 cnvxp 6178 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
259258reseq1i 5995 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))})
260 ssid 4017 . . . . . . . . . . . . . . . . . . . . . . . 24 {(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))}
261 xpssres 6037 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))} → (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋))
262260, 261ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
263259, 262eqtri 2762 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
264263rneqi 5950 . . . . . . . . . . . . . . . . . . . . 21 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
26546snnz 4780 . . . . . . . . . . . . . . . . . . . . . 22 {(𝑋𝐹(𝑊𝑋))} ≠ ∅
266 rnxp 6191 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑋𝐹(𝑊𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋)
267265, 266ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋
268264, 267eqtri 2762 . . . . . . . . . . . . . . . . . . . 20 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
269257, 268eqtri 2762 . . . . . . . . . . . . . . . . . . 19 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
270256, 269eqtrdi 2790 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = 𝑋)
271254, 270uneq12d 4178 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
272 cnvun 6164 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) = ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
273272imaeq1i 6076 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})
274 imaundir 6172 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
275273, 274eqtri 2762 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
276 un0 4399 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = 𝑋
277 uncom 4167 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
278276, 277eqtr3i 2764 . . . . . . . . . . . . . . . . 17 𝑋 = (∅ ∪ 𝑋)
279271, 275, 2783eqtr4g 2799 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = 𝑋)
280189, 279sylan9eqr 2796 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
281280sqxpeqd 5720 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
282281ineq2d 4227 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)))
283 indir 4291 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)))
284 dfss2 3980 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
285244, 284sylib 218 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
286 incom 4216 . . . . . . . . . . . . . . . . . . . . . . 23 ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))})
287 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
288242, 287sylibr 234 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
289286, 288eqtrid 2786 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = ∅)
290289xpeq2d 5718 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
291 xpindi 5846 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))
292 xp0 6179 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ∅) = ∅
293290, 291, 2923eqtr3g 2797 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
294285, 293uneq12d 4178 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊𝑋) ∪ ∅))
295283, 294eqtrid 2786 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊𝑋) ∪ ∅))
296 un0 4399 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) ∪ ∅) = (𝑊𝑋)
297295, 296eqtrdi 2790 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
298297adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
299282, 298eqtrd 2774 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊𝑋))
300280, 299oveq12d 7448 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊𝑋)))
301300eqeq1d 2736 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
302241, 301sbcied 3836 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
303240, 302mpbird 257 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
304238, 303jaodan 959 . . . . . . . . . 10 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
305135, 304sylan2b 594 . . . . . . . . 9 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
306305ralrimiva 3143 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307175, 306jca 511 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
3082, 3fpwwe2lem2 10669 . . . . . . . 8 (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
309308adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
31034, 307, 309mpbir2and 713 . . . . . 6 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
3112relopabiv 5832 . . . . . . 7 Rel 𝑊
312311releldmi 5961 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊)
313 elssuni 4941 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
314310, 312, 3133syl 18 . . . . 5 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
315314, 7sseqtrrdi 4046 . . . 4 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
3161, 315sstrid 4006 . . 3 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
31746snss 4789 . . 3 ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
318316, 317sylibr 234 . 2 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
319318pm2.18da 800 1 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3o 1085  w3a 1086  wal 1534   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  [wsbc 3790  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604  {csn 4630   cuni 4911   class class class wbr 5147  {copab 5209   Or wor 5595   Fr wfr 5637   We wwe 5639   × cxp 5686  ccnv 5687  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  Fun wfun 6556  wf 6558  cfv 6562  (class class class)co 7430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-oi 9547
This theorem is referenced by:  fpwwe2  10680
  Copyright terms: Public domain W3C validator