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

Theorem fpwwe2lem12 10578
Description: Lemma for fpwwe2 10579. (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 4133 . . . 4 {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
2 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . . . . . . . 15 (𝜑𝐴𝑉)
43adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝐴𝑉)
5 fpwwe2.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
65adantlr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
7 fpwwe2.4 . . . . . . . . . . . . . 14 𝑋 = dom 𝑊
82, 4, 6, 7fpwwe2lem11 10577 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋 ∈ dom 𝑊)
92, 4, 6, 7fpwwe2lem10 10576 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
10 ffun 6671 . . . . . . . . . . . . . 14 (𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋) → Fun 𝑊)
11 funfvbrb 7001 . . . . . . . . . . . . . 14 (Fun 𝑊 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
129, 10, 113syl 18 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
138, 12mpbid 231 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝑊(𝑊𝑋))
142, 4fpwwe2lem2 10568 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝑊(𝑊𝑋) ↔ ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
1513, 14mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
1615simpld 495 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)))
1716simpld 495 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑋𝐴)
1816simprd 496 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
1915simprd 496 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
2019simpld 495 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) We 𝑋)
2117, 18, 203jca 1128 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋))
222, 3, 5fpwwe2lem4 10570 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋) ∧ (𝑊𝑋) We 𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2321, 22syldan 591 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝐴)
2423snssd 4769 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝐴)
2517, 24unssd 4146 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴)
26 ssun1 4132 . . . . . . . . . . 11 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})
27 xpss12 5648 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
2826, 26, 27mp2an 690 . . . . . . . . . 10 (𝑋 × 𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
2918, 28sstrdi 3956 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
30 xpss12 5648 . . . . . . . . . . 11 ((𝑋 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ {(𝑋𝐹(𝑊𝑋))} ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3126, 1, 30mp2an 690 . . . . . . . . . 10 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
3231a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3329, 32unssd 4146 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})))
3425, 33jca 512 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))))
35 ssdif0 4323 . . . . . . . . . . . . . 14 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅)
36 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
3718ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
3837ssbrd 5148 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋))))
39 brxp 5681 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4039simplbi 498 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4138, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
4236, 41mtod 197 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)))
43 brxp 5681 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ∧ (𝑋𝐹(𝑊𝑋)) ∈ {(𝑋𝐹(𝑊𝑋))}))
4443simplbi 498 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
4536, 44nsyl 140 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))
46 ovex 7390 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐹(𝑊𝑋)) ∈ V
47 breq2 5109 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋))))
48 brun 5156 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))(𝑋𝐹(𝑊𝑋)) ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
4947, 48bitrdi 286 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑋𝐹(𝑊𝑋)) → ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5049notbid 317 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑋𝐹(𝑊𝑋)) → (¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋)))))
5146, 50rexsn 4643 . . . . . . . . . . . . . . . . . 18 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
52 ioran 982 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5351, 52bitri 274 . . . . . . . . . . . . . . . . 17 (∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)(𝑋𝐹(𝑊𝑋)) ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})(𝑋𝐹(𝑊𝑋))))
5442, 45, 53sylanbrc 583 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
55 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))})
56 sssn 4786 . . . . . . . . . . . . . . . . . . 19 (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} ↔ (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
5755, 56sylib 217 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (𝑥 = ∅ ∨ 𝑥 = {(𝑋𝐹(𝑊𝑋))}))
58 simplrr 776 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 ≠ ∅)
5958neneqd 2948 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑥 = ∅)
6057, 59orcnd 877 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = {(𝑋𝐹(𝑊𝑋))})
6160raleqdv 3313 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
62 breq1 5108 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6362notbid 317 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6446, 63ralsn 4642 . . . . . . . . . . . . . . . . . 18 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6561, 64bitrdi 286 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6660, 65rexeqbidv 3320 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → (∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ∃𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ (𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6754, 66mpbird 256 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ 𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))}) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
6867ex 413 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → (𝑥 ⊆ {(𝑋𝐹(𝑊𝑋))} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
6935, 68biimtrrid 242 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) = ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
70 vex 3449 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
71 difexg 5284 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
7270, 71mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V)
73 wefr 5623 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Fr 𝑋)
7420, 73syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Fr 𝑋)
7574ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑊𝑋) Fr 𝑋)
76 simplrl 775 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
77 uncom 4113 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋)
7876, 77sseqtrdi 3994 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → 𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋))
79 ssundif 4445 . . . . . . . . . . . . . . . . 17 (𝑥 ⊆ ({(𝑋𝐹(𝑊𝑋))} ∪ 𝑋) ↔ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
8078, 79sylib 217 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
81 simpr 485 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)
82 fri 5593 . . . . . . . . . . . . . . . 16 ((((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋 ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅)) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
8372, 75, 80, 81, 82syl22anc 837 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦)
84 brun 5156 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
85 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑊𝑋)𝑦𝑧(𝑊𝑋)𝑦))
86 brxp 5681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑧𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
8786simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
88 eldifn 4087 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
8988adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
9089pm2.21d 121 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑧(𝑊𝑋)𝑦))
9187, 90syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦))
9285, 91jaod 857 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) → 𝑧(𝑊𝑋)𝑦))
9384, 92biimtrid 241 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
9493con3d 152 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (¬ 𝑧(𝑊𝑋)𝑦 → ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
9594ralimdv 3166 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
96 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9796ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
9818ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
9998ssbrd 5148 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦))
100 brxp 5681 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦𝑋))
101100simplbi 498 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × 𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
10299, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
10397, 102mtod 197 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦)
104 brxp 5681 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
105104simprbi 497 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})
10689, 105nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
107 brun 5156 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐹(𝑊𝑋))((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
10862, 107bitrdi 286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
109108notbid 317 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑋𝐹(𝑊𝑋)) → (¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)))
11046, 109ralsn 4642 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ ¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
111 ioran 982 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∨ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦) ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
112110, 111bitri 274 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ↔ (¬ (𝑋𝐹(𝑊𝑋))(𝑊𝑋)𝑦 ∧ ¬ (𝑋𝐹(𝑊𝑋))(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
113103, 106, 112sylanbrc 583 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
11495, 113jctird 527 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
115 ssun1 4132 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ⊆ (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
116 undif1 4435 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) = (𝑥 ∪ {(𝑋𝐹(𝑊𝑋))})
117115, 116sseqtrri 3981 . . . . . . . . . . . . . . . . . . . 20 𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))})
118 ralun 4152 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
119 ssralv 4010 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ⊆ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) → (∀𝑧 ∈ ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∪ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
120117, 118, 119mpsyl 68 . . . . . . . . . . . . . . . . . . 19 ((∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 ∧ ∀𝑧 ∈ {(𝑋𝐹(𝑊𝑋))} ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦) → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
121114, 120syl6 35 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
122 eldifi 4086 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) → 𝑦𝑥)
123122adantl 482 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → 𝑦𝑥)
124121, 123jctild 526 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) ∧ 𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})) → (∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
125124expimpd 454 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ((𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦) → (𝑦𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)))
126125reximdv2 3161 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → (∃𝑦 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))})∀𝑧 ∈ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ¬ 𝑧(𝑊𝑋)𝑦 → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
12783, 126mpd 15 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) ∧ (𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
128127ex 413 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {(𝑋𝐹(𝑊𝑋))}) ≠ ∅ → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
12969, 128pm2.61dne 3031 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅)) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
130129ex 413 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
131130alrimiv 1930 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
132 df-fr 5588 . . . . . . . . . 10 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ ∀𝑥((𝑥 ⊆ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
133131, 132sylibr 233 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
134 elun 4108 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
135 elun 4108 . . . . . . . . . . . 12 (𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
136134, 135anbi12i 627 . . . . . . . . . . 11 ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) ↔ ((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})))
137 weso 5624 . . . . . . . . . . . . . . . 16 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Or 𝑋)
13820, 137syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑊𝑋) Or 𝑋)
139 solin 5570 . . . . . . . . . . . . . . 15 (((𝑊𝑋) Or 𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
140138, 139sylan 580 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥))
141 ssun1 4132 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
142141a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑊𝑋) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
143142ssbrd 5148 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥(𝑊𝑋)𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
144 idd 24 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑦𝑥 = 𝑦))
145142ssbrd 5148 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑦(𝑊𝑋)𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
146143, 144, 1453orim123d 1444 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥(𝑊𝑋)𝑦𝑥 = 𝑦𝑦(𝑊𝑋)𝑥) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
147140, 146mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
148147ex 413 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
149 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋))
150149ancomd 462 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
151 brxp 5681 . . . . . . . . . . . . . . 15 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥 ↔ (𝑦𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}))
152150, 151sylibr 233 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → 𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥)
153 ssun2 4133 . . . . . . . . . . . . . . 15 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ⊆ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
154153ssbri 5150 . . . . . . . . . . . . . 14 (𝑦(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑥𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)
155 3mix3 1332 . . . . . . . . . . . . . 14 (𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
156152, 154, 1553syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋)) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
157156ex 413 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦𝑋) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
158 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
159 brxp 5681 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 ↔ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}))
160158, 159sylibr 233 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → 𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
161153ssbri 5150 . . . . . . . . . . . . . 14 (𝑥(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
162 3mix1 1330 . . . . . . . . . . . . . 14 (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦 → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
163160, 161, 1623syl 18 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
164163ex 413 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
165 elsni 4603 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑥 = (𝑋𝐹(𝑊𝑋)))
166 elsni 4603 . . . . . . . . . . . . . . 15 (𝑦 ∈ {(𝑋𝐹(𝑊𝑋))} → 𝑦 = (𝑋𝐹(𝑊𝑋)))
167 eqtr3 2762 . . . . . . . . . . . . . . 15 ((𝑥 = (𝑋𝐹(𝑊𝑋)) ∧ 𝑦 = (𝑋𝐹(𝑊𝑋))) → 𝑥 = 𝑦)
168165, 166, 167syl2an 596 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑥 = 𝑦)
1691683mix2d 1337 . . . . . . . . . . . . 13 ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
170169a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ {(𝑋𝐹(𝑊𝑋))} ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
171148, 157, 164, 170ccased 1037 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑥𝑋𝑥 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
172136, 171biimtrid 241 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → (𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
173172ralrimivv 3195 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥))
174 dfwe2 7708 . . . . . . . . 9 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ↔ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) Fr (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑥 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})(𝑥((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑥 = 𝑦𝑦((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑥)))
175133, 173, 174sylanbrc 583 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))
1762fpwwe2cbv 10566 . . . . . . . . . . . . 13 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 × 𝑏))) = 𝑧))}
177176, 4, 13fpwwe2lem3 10569 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦)
178 cnvimass 6033 . . . . . . . . . . . . . . 15 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
179 fvex 6855 . . . . . . . . . . . . . . . . 17 (𝑊𝑋) ∈ V
180 snex 5388 . . . . . . . . . . . . . . . . . 18 {(𝑋𝐹(𝑊𝑋))} ∈ V
181 xpexg 7684 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ dom 𝑊 ∧ {(𝑋𝐹(𝑊𝑋))} ∈ V) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
1828, 180, 181sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V)
183 unexg 7683 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∈ V ∧ (𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∈ V) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
184179, 182, 183sylancr 587 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
185184dmexd 7842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V)
186 ssexg 5280 . . . . . . . . . . . . . . 15 (((((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ⊆ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∧ dom ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∈ V) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
187178, 185, 186sylancr 587 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
188187adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
189 id 22 . . . . . . . . . . . . . . . 16 (𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) → 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}))
190 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦𝑋)
191 simplr 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
192 nelne2 3042 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑋 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
193190, 191, 192syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → 𝑦 ≠ (𝑋𝐹(𝑊𝑋)))
19487, 166syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑦 = (𝑋𝐹(𝑊𝑋)))
195194necon3ai 2968 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ≠ (𝑋𝐹(𝑊𝑋)) → ¬ 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦)
196 biorf 935 . . . . . . . . . . . . . . . . . . . 20 𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦 → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
197193, 195, 1963syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧(𝑊𝑋)𝑦 ↔ (𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦)))
198 orcom 868 . . . . . . . . . . . . . . . . . . . 20 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ (𝑧(𝑊𝑋)𝑦𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦))
199198, 84bitr4i 277 . . . . . . . . . . . . . . . . . . 19 ((𝑧(𝑋 × {(𝑋𝐹(𝑊𝑋))})𝑦𝑧(𝑊𝑋)𝑦) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
200197, 199bitr2di 287 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦𝑧(𝑊𝑋)𝑦))
201 vex 3449 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
202201eliniseg 6046 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦))
203202elv 3451 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))𝑦)
204201eliniseg 6046 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦))
205204elv 3451 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝑊𝑋) “ {𝑦}) ↔ 𝑧(𝑊𝑋)𝑦)
206200, 203, 2053bitr4g 313 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑧 ∈ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ↔ 𝑧 ∈ ((𝑊𝑋) “ {𝑦})))
207206eqrdv 2734 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = ((𝑊𝑋) “ {𝑦}))
208189, 207sylan9eqr 2798 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = ((𝑊𝑋) “ {𝑦}))
209208sqxpeqd 5665 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
210209ineq2d 4172 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
211 indir 4235 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
212 inxp 5788 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})))
213 incom 4161 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))})
214 cnvimass 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑊𝑋) “ {𝑦}) ⊆ dom (𝑊𝑋)
21518adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
216 dmss 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
217215, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
218 dmxpid 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑋 × 𝑋) = 𝑋
219217, 218sseqtrdi 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → dom (𝑊𝑋) ⊆ 𝑋)
220214, 219sstrid 3955 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑊𝑋) “ {𝑦}) ⊆ 𝑋)
221220, 191ssneldd 3947 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
222 disjsn 4672 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ ((𝑊𝑋) “ {𝑦}))
223221, 222sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) “ {𝑦}) ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
224213, 223eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦})) = ∅)
225224xpeq2d 5663 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅))
226 xp0 6110 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ∅) = ∅
227225, 226eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑦})) × ({(𝑋𝐹(𝑊𝑋))} ∩ ((𝑊𝑋) “ {𝑦}))) = ∅)
228212, 227eqtrid 2788 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ∅)
229228uneq2d 4123 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
230211, 229eqtrid 2788 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅))
231 un0 4350 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) ∪ ∅) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))
232230, 231eqtrdi 2792 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
233232adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
234210, 233eqtrd 2776 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦}))))
235208, 234oveq12d 7375 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))))
236235eqeq1d 2738 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
237188, 236sbcied 3784 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (((𝑊𝑋) “ {𝑦})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑦}) × ((𝑊𝑋) “ {𝑦})))) = 𝑦))
238177, 237mpbird 256 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦𝑋) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
239166adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → 𝑦 = (𝑋𝐹(𝑊𝑋)))
240239eqcomd 2742 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋𝐹(𝑊𝑋)) = 𝑦)
241187adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) ∈ V)
242 simplr 767 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
243239eleq1d 2822 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) ↔ (𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋)))
24418adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
245 rnss 5894 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ran (𝑊𝑋) ⊆ ran (𝑋 × 𝑋))
247 df-rn 5644 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑊𝑋) = dom (𝑊𝑋)
248 rnxpid 6125 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × 𝑋) = 𝑋
249246, 247, 2483sstr3g 3988 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → dom (𝑊𝑋) ⊆ 𝑋)
250249sseld 3943 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋𝐹(𝑊𝑋)) ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
251243, 250sylbid 239 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑦 ∈ dom (𝑊𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
252242, 251mtod 197 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ¬ 𝑦 ∈ dom (𝑊𝑋))
253 ndmima 6055 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ dom (𝑊𝑋) → ((𝑊𝑋) “ {𝑦}) = ∅)
254252, 253syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) “ {𝑦}) = ∅)
255239sneqd 4598 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → {𝑦} = {(𝑋𝐹(𝑊𝑋))})
256255imaeq2d 6013 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}))
257 df-ima 5646 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))})
258 cnvxp 6109 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 × {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
259258reseq1i 5933 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))})
260 ssid 3966 . . . . . . . . . . . . . . . . . . . . . . . 24 {(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))}
261 xpssres 5974 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(𝑊𝑋))} ⊆ {(𝑋𝐹(𝑊𝑋))} → (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋))
262260, 261ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (({(𝑋𝐹(𝑊𝑋))} × 𝑋) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
263259, 262eqtri 2764 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
264263rneqi 5892 . . . . . . . . . . . . . . . . . . . . 21 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋)
26546snnz 4737 . . . . . . . . . . . . . . . . . . . . . 22 {(𝑋𝐹(𝑊𝑋))} ≠ ∅
266 rnxp 6122 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑋𝐹(𝑊𝑋))} ≠ ∅ → ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋)
267265, 266ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ran ({(𝑋𝐹(𝑊𝑋))} × 𝑋) = 𝑋
268264, 267eqtri 2764 . . . . . . . . . . . . . . . . . . . 20 ran ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ↾ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
269257, 268eqtri 2764 . . . . . . . . . . . . . . . . . . 19 ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {(𝑋𝐹(𝑊𝑋))}) = 𝑋
270256, 269eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}) = 𝑋)
271254, 270uneq12d 4124 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦})) = (∅ ∪ 𝑋))
272 cnvun 6095 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) = ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))}))
273272imaeq1i 6010 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})
274 imaundir 6103 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
275273, 274eqtri 2764 . . . . . . . . . . . . . . . . 17 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = (((𝑊𝑋) “ {𝑦}) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) “ {𝑦}))
276 un0 4350 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = 𝑋
277 uncom 4113 . . . . . . . . . . . . . . . . . 18 (𝑋 ∪ ∅) = (∅ ∪ 𝑋)
278276, 277eqtr3i 2766 . . . . . . . . . . . . . . . . 17 𝑋 = (∅ ∪ 𝑋)
279271, 275, 2783eqtr4g 2801 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) = 𝑋)
280189, 279sylan9eqr 2798 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → 𝑢 = 𝑋)
281280sqxpeqd 5665 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢 × 𝑢) = (𝑋 × 𝑋))
282281ineq2d 4172 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)))
283 indir 4235 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)))
284 df-ss 3927 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) ↔ ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
285244, 284sylib 217 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑊𝑋) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
286 incom 4161 . . . . . . . . . . . . . . . . . . . . . . 23 ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))})
287 disjsn 4672 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅ ↔ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
288242, 287sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 ∩ {(𝑋𝐹(𝑊𝑋))}) = ∅)
289286, 288eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋) = ∅)
290289xpeq2d 5663 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = (𝑋 × ∅))
291 xpindi 5789 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ({(𝑋𝐹(𝑊𝑋))} ∩ 𝑋)) = ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))
292 xp0 6110 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 × ∅) = ∅
293290, 291, 2923eqtr3g 2799 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋)) = ∅)
294285, 293uneq12d 4124 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∩ (𝑋 × 𝑋)) ∪ ((𝑋 × {(𝑋𝐹(𝑊𝑋))}) ∩ (𝑋 × 𝑋))) = ((𝑊𝑋) ∪ ∅))
295283, 294eqtrid 2788 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = ((𝑊𝑋) ∪ ∅))
296 un0 4350 . . . . . . . . . . . . . . . . . 18 ((𝑊𝑋) ∪ ∅) = (𝑊𝑋)
297295, 296eqtrdi 2792 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
298297adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑋 × 𝑋)) = (𝑊𝑋))
299282, 298eqtrd 2776 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢)) = (𝑊𝑋))
300280, 299oveq12d 7375 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → (𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = (𝑋𝐹(𝑊𝑋)))
301300eqeq1d 2738 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) ∧ 𝑢 = (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦})) → ((𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
302241, 301sbcied 3784 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → ([(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑋𝐹(𝑊𝑋)) = 𝑦))
303240, 302mpbird 256 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(𝑊𝑋))}) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
304238, 303jaodan 956 . . . . . . . . . 10 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ (𝑦𝑋𝑦 ∈ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
305135, 304sylan2b 594 . . . . . . . . 9 (((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})) → [(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
306305ralrimiva 3143 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦)
307175, 306jca 512 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))
3082, 3fpwwe2lem2 10568 . . . . . . . 8 (𝜑 → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
309308adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ↔ (((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝐴 ∧ ((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ⊆ ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) × (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}))) ∧ (((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) We (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∧ ∀𝑦 ∈ (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})[(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) “ {𝑦}) / 𝑢](𝑢𝐹(((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) ∩ (𝑢 × 𝑢))) = 𝑦))))
31034, 307, 309mpbir2and 711 . . . . . 6 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})))
3112relopabiv 5776 . . . . . . 7 Rel 𝑊
312311releldmi 5903 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))})𝑊((𝑊𝑋) ∪ (𝑋 × {(𝑋𝐹(𝑊𝑋))})) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊)
313 elssuni 4898 . . . . . 6 ((𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ∈ dom 𝑊 → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
314310, 312, 3133syl 18 . . . . 5 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ dom 𝑊)
315314, 7sseqtrrdi 3995 . . . 4 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋 ∪ {(𝑋𝐹(𝑊𝑋))}) ⊆ 𝑋)
3161, 315sstrid 3955 . . 3 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
31746snss 4746 . . 3 ((𝑋𝐹(𝑊𝑋)) ∈ 𝑋 ↔ {(𝑋𝐹(𝑊𝑋))} ⊆ 𝑋)
318316, 317sylibr 233 . 2 ((𝜑 ∧ ¬ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋) → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
319318pm2.18da 798 1 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087  wal 1539   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  [wsbc 3739  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   cuni 4865   class class class wbr 5105  {copab 5167   Or wor 5544   Fr wfr 5585   We wwe 5587   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-oi 9446
This theorem is referenced by:  fpwwe2  10579
  Copyright terms: Public domain W3C validator