MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2lem12 Structured version   Visualization version   GIF version
Theorem fpwwe2lem12 10634
Description: Lemma for fpwwe2 10635. (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 4173 . . . 4 {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
2 fpwwe2.1 . . . . . . . . . . . . . 14 π‘Š = {⟨π‘₯, π‘ŸβŸ© ∣ ((π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯)) ∧ (π‘Ÿ We π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ [(β—‘π‘Ÿ β€œ {𝑦}) / 𝑒](𝑒𝐹(π‘Ÿ ∩ (𝑒 Γ— 𝑒))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 ∈ 𝑉)
43adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝐴 ∈ 𝑉)
5 fpwwe2.3 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯)) β†’ (π‘₯πΉπ‘Ÿ) ∈ 𝐴)
65adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯)) β†’ (π‘₯πΉπ‘Ÿ) ∈ 𝐴)
7 fpwwe2.4 . . . . . . . . . . . . . 14 𝑋 = βˆͺ dom π‘Š
82, 4, 6, 7fpwwe2lem11 10633 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝑋 ∈ dom π‘Š)
92, 4, 6, 7fpwwe2lem10 10632 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ π‘Š:dom π‘ŠβŸΆπ’« (𝑋 Γ— 𝑋))
10 ffun 6718 . . . . . . . . . . . . . 14 (π‘Š:dom π‘ŠβŸΆπ’« (𝑋 Γ— 𝑋) β†’ Fun π‘Š)
11 funfvbrb 7050 . . . . . . . . . . . . . 14 (Fun π‘Š β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
129, 10, 113syl 18 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
138, 12mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
142, 4fpwwe2lem2 10624 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ↔ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
1513, 14mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
1615simpld 496 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)))
1716simpld 496 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝑋 βŠ† 𝐴)
1816simprd 497 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
1915simprd 497 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))
2019simpld 496 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) We 𝑋)
2117, 18, 203jca 1129 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) ∧ (π‘Šβ€˜π‘‹) We 𝑋))
222, 3, 5fpwwe2lem4 10626 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) ∧ (π‘Šβ€˜π‘‹) We 𝑋)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝐴)
2321, 22syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝐴)
2423snssd 4812 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† 𝐴)
2517, 24unssd 4186 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴)
26 ssun1 4172 . . . . . . . . . . 11 𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
27 xpss12 5691 . . . . . . . . . . 11 ((𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑋 Γ— 𝑋) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
2826, 26, 27mp2an 691 . . . . . . . . . 10 (𝑋 Γ— 𝑋) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
2918, 28sstrdi 3994 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
30 xpss12 5691 . . . . . . . . . . 11 ((𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3126, 1, 30mp2an 691 . . . . . . . . . 10 (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
3231a1i 11 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3329, 32unssd 4186 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3425, 33jca 513 . . . . . . 7 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴 ∧ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))))
35 ssdif0 4363 . . . . . . . . . . . . . 14 (π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} ↔ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ…)
36 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
3718ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
3837ssbrd 5191 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)(𝑋𝐹(π‘Šβ€˜π‘‹))))
39 brxp 5724 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)(𝑋𝐹(π‘Šβ€˜π‘‹)) ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
4039simplbi 499 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
4138, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
4236, 41mtod 197 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)))
43 brxp 5724 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)) ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
4443simplbi 499 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
4536, 44nsyl 140 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)))
46 ovex 7439 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ V
47 breq2 5152 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))(𝑋𝐹(π‘Šβ€˜π‘‹))))
48 brun 5199 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))(𝑋𝐹(π‘Šβ€˜π‘‹)) ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
4947, 48bitrdi 287 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)))))
5049notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)))))
5146, 50rexsn 4686 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
52 ioran 983 . . . . . . . . . . . . . . . . . 18 (Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))) ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
5351, 52bitri 275 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
5442, 45, 53sylanbrc 584 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
55 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))})
56 sssn 4829 . . . . . . . . . . . . . . . . . . 19 (π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} ↔ (π‘₯ = βˆ… ∨ π‘₯ = {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
5755, 56sylib 217 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯ = βˆ… ∨ π‘₯ = {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
58 simplrr 777 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ β‰  βˆ…)
5958neneqd 2946 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ π‘₯ = βˆ…)
6057, 59orcnd 878 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ = {(𝑋𝐹(π‘Šβ€˜π‘‹))})
6160raleqdv 3326 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
62 breq1 5151 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6362notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6446, 63ralsn 4685 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
6561, 64bitrdi 287 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6660, 65rexeqbidv 3344 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6754, 66mpbird 257 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
6867ex 414 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ (π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6935, 68biimtrrid 242 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ… β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
70 vex 3479 . . . . . . . . . . . . . . . . 17 π‘₯ ∈ V
71 difexg 5327 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ V β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
7270, 71mp1i 13 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
73 wefr 5666 . . . . . . . . . . . . . . . . . 18 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
7420, 73syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
7574ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
76 simplrl 776 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
77 uncom 4153 . . . . . . . . . . . . . . . . . 18 (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βˆͺ 𝑋)
7876, 77sseqtrdi 4032 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ π‘₯ βŠ† ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βˆͺ 𝑋))
79 ssundif 4487 . . . . . . . . . . . . . . . . 17 (π‘₯ βŠ† ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βˆͺ 𝑋) ↔ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋)
8078, 79sylib 217 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋)
81 simpr 486 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…)
82 fri 5636 . . . . . . . . . . . . . . . 16 ((((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V ∧ (π‘Šβ€˜π‘‹) Fr 𝑋) ∧ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋 ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…)) β†’ βˆƒπ‘¦ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦)
8372, 75, 80, 81, 82syl22anc 838 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦)
84 brun 5199 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (𝑧(π‘Šβ€˜π‘‹)𝑦 ∨ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
85 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
86 brxp 5724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ↔ (𝑧 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
8786simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
88 eldifn 4127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
8988adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
9089pm2.21d 121 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9187, 90syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9285, 91jaod 858 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ ((𝑧(π‘Šβ€˜π‘‹)𝑦 ∨ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦) β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9384, 92biimtrid 241 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9493con3d 152 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
9594ralimdv 3170 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
96 simpr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
9796ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
9818ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
9998ssbrd 5191 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 β†’ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)𝑦))
100 brxp 5724 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))
101100simplbi 499 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)𝑦 β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
10299, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
10397, 102mtod 197 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦)
104 brxp 5724 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
105104simprbi 498 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
10689, 105nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)
107 brun 5199 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
10862, 107bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)))
109108notbid 318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)))
11046, 109ralsn 4685 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
111 ioran 983 . . . . . . . . . . . . . . . . . . . . . 22 (Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦) ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
112110, 111bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
113103, 106, 112sylanbrc 584 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
11495, 113jctird 528 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∧ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)))
115 ssun1 4172 . . . . . . . . . . . . . . . . . . . . 21 π‘₯ βŠ† (π‘₯ βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
116 undif1 4475 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = (π‘₯ βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
117115, 116sseqtrri 4019 . . . . . . . . . . . . . . . . . . . 20 π‘₯ βŠ† ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
118 ralun 4192 . . . . . . . . . . . . . . . . . . . 20 ((βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∧ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦) β†’ βˆ€π‘§ ∈ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
119 ssralv 4050 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ βŠ† ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆ€π‘§ ∈ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 β†’ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
120117, 118, 119mpsyl 68 . . . . . . . . . . . . . . . . . . 19 ((βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∧ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦) β†’ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
121114, 120syl6 35 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
122 eldifi 4126 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ 𝑦 ∈ π‘₯)
123122adantl 483 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ 𝑦 ∈ π‘₯)
124121, 123jctild 527 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ (𝑦 ∈ π‘₯ ∧ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)))
125124expimpd 455 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ ((𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦) β†’ (𝑦 ∈ π‘₯ ∧ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)))
126125reximdv2 3165 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (βˆƒπ‘¦ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
12783, 126mpd 15 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
128127ex 414 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ… β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
12969, 128pm2.61dne 3029 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
130129ex 414 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
131130alrimiv 1931 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ βˆ€π‘₯((π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
132 df-fr 5631 . . . . . . . . . 10 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) Fr (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ βˆ€π‘₯((π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
133131, 132sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) Fr (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
134 elun 4148 . . . . . . . . . . . 12 (π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ (π‘₯ ∈ 𝑋 ∨ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
135 elun 4148 . . . . . . . . . . . 12 (𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
136134, 135anbi12i 628 . . . . . . . . . . 11 ((π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ↔ ((π‘₯ ∈ 𝑋 ∨ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
137 weso 5667 . . . . . . . . . . . . . . . 16 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
13820, 137syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
139 solin 5613 . . . . . . . . . . . . . . 15 (((π‘Šβ€˜π‘‹) Or 𝑋 ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯(π‘Šβ€˜π‘‹)𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦(π‘Šβ€˜π‘‹)π‘₯))
140138, 139sylan 581 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯(π‘Šβ€˜π‘‹)𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦(π‘Šβ€˜π‘‹)π‘₯))
141 ssun1 4172 . . . . . . . . . . . . . . . . 17 (π‘Šβ€˜π‘‹) βŠ† ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
142141a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Šβ€˜π‘‹) βŠ† ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
143142ssbrd 5191 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯(π‘Šβ€˜π‘‹)𝑦 β†’ π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
144 idd 24 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯ = 𝑦 β†’ π‘₯ = 𝑦))
145142ssbrd 5191 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦(π‘Šβ€˜π‘‹)π‘₯ β†’ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
146143, 144, 1453orim123d 1445 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘₯(π‘Šβ€˜π‘‹)𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦(π‘Šβ€˜π‘‹)π‘₯) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
147140, 146mpd 15 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
148147ex 414 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
149 simpr 486 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋))
150149ancomd 463 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦 ∈ 𝑋 ∧ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
151 brxp 5724 . . . . . . . . . . . . . . 15 (𝑦(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘₯ ↔ (𝑦 ∈ 𝑋 ∧ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
152150, 151sylibr 233 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ 𝑦(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘₯)
153 ssun2 4173 . . . . . . . . . . . . . . 15 (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
154153ssbri 5193 . . . . . . . . . . . . . 14 (𝑦(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘₯ β†’ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)
155 3mix3 1333 . . . . . . . . . . . . . 14 (𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯ β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
156152, 154, 1553syl 18 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
157156ex 414 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
158 simpr 486 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
159 brxp 5724 . . . . . . . . . . . . . . 15 (π‘₯(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ↔ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
160158, 159sylibr 233 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ π‘₯(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)
161153ssbri 5193 . . . . . . . . . . . . . 14 (π‘₯(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
162 3mix1 1331 . . . . . . . . . . . . . 14 (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
163160, 161, 1623syl 18 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
164163ex 414 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
165 elsni 4645 . . . . . . . . . . . . . . 15 (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ π‘₯ = (𝑋𝐹(π‘Šβ€˜π‘‹)))
166 elsni 4645 . . . . . . . . . . . . . . 15 (𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)))
167 eqtr3 2759 . . . . . . . . . . . . . . 15 ((π‘₯ = (𝑋𝐹(π‘Šβ€˜π‘‹)) ∧ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹))) β†’ π‘₯ = 𝑦)
168165, 166, 167syl2an 597 . . . . . . . . . . . . . 14 ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ = 𝑦)
1691683mix2d 1338 . . . . . . . . . . . . 13 ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
170169a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
171148, 157, 164, 170ccased 1038 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (((π‘₯ ∈ 𝑋 ∨ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
172136, 171biimtrid 241 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
173172ralrimivv 3199 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ βˆ€π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})(π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
174 dfwe2 7758 . . . . . . . . 9 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) Fr (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})(π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
175133, 173, 174sylanbrc 584 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
1762fpwwe2cbv 10622 . . . . . . . . . . . . 13 π‘Š = {βŸ¨π‘Ž, π‘ βŸ© ∣ ((π‘Ž βŠ† 𝐴 ∧ 𝑠 βŠ† (π‘Ž Γ— π‘Ž)) ∧ (𝑠 We π‘Ž ∧ βˆ€π‘§ ∈ π‘Ž [(◑𝑠 β€œ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 Γ— 𝑏))) = 𝑧))}
177176, 4, 13fpwwe2lem3 10625 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = 𝑦)
178 cnvimass 6078 . . . . . . . . . . . . . . 15 (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) βŠ† dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
179 fvex 6902 . . . . . . . . . . . . . . . . 17 (π‘Šβ€˜π‘‹) ∈ V
180 snex 5431 . . . . . . . . . . . . . . . . . 18 {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∈ V
181 xpexg 7734 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ dom π‘Š ∧ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∈ V) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
1828, 180, 181sylancl 587 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
183 unexg 7733 . . . . . . . . . . . . . . . . 17 (((π‘Šβ€˜π‘‹) ∈ V ∧ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V)
184179, 182, 183sylancr 588 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V)
185184dmexd 7893 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V)
186 ssexg 5323 . . . . . . . . . . . . . . 15 (((β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) βŠ† dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∧ dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
187178, 185, 186sylancr 588 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
188187adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
189 id 22 . . . . . . . . . . . . . . . 16 (𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) β†’ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}))
190 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ 𝑦 ∈ 𝑋)
191 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
192 nelne2 3041 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ 𝑋 ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝑦 β‰  (𝑋𝐹(π‘Šβ€˜π‘‹)))
193190, 191, 192syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ 𝑦 β‰  (𝑋𝐹(π‘Šβ€˜π‘‹)))
19487, 166syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)))
195194necon3ai 2966 . . . . . . . . . . . . . . . . . . . 20 (𝑦 β‰  (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ Β¬ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)
196 biorf 936 . . . . . . . . . . . . . . . . . . . 20 (Β¬ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ (𝑧(π‘Šβ€˜π‘‹)𝑦 ↔ (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦)))
197193, 195, 1963syl 18 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (𝑧(π‘Šβ€˜π‘‹)𝑦 ↔ (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦)))
198 orcom 869 . . . . . . . . . . . . . . . . . . . 20 ((𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦) ↔ (𝑧(π‘Šβ€˜π‘‹)𝑦 ∨ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
199198, 84bitr4i 278 . . . . . . . . . . . . . . . . . . 19 ((𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦) ↔ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
200197, 199bitr2di 288 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑦))
201 vex 3479 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
202201eliniseg 6091 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V β†’ (𝑧 ∈ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ↔ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
203202elv 3481 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ↔ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
204201eliniseg 6091 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V β†’ (𝑧 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ↔ 𝑧(π‘Šβ€˜π‘‹)𝑦))
205204elv 3481 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ↔ 𝑧(π‘Šβ€˜π‘‹)𝑦)
206200, 203, 2053bitr4g 314 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (𝑧 ∈ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ↔ 𝑧 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
207206eqrdv 2731 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
208189, 207sylan9eqr 2795 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ 𝑒 = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
209208sqxpeqd 5708 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒 Γ— 𝑒) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
210209ineq2d 4212 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
211 indir 4275 . . . . . . . . . . . . . . . . . . 19 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
212 inxp 5831 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
213 incom 4201 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
214 cnvimass 6078 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βŠ† dom (π‘Šβ€˜π‘‹)
21518adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
216 dmss 5901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
217215, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
218 dmxpid 5928 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑋 Γ— 𝑋) = 𝑋
219217, 218sseqtrdi 4032 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† 𝑋)
220214, 219sstrid 3993 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βŠ† 𝑋)
221220, 191ssneldd 3985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
222 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ… ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
223221, 222sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ…)
224213, 223eqtrid 2785 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) = βˆ…)
225224xpeq2d 5706 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— βˆ…))
226 xp0 6155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— βˆ…) = βˆ…
227225, 226eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = βˆ…)
228212, 227eqtrid 2785 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = βˆ…)
229228uneq2d 4163 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ βˆ…))
230211, 229eqtrid 2785 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ βˆ…))
231 un0 4390 . . . . . . . . . . . . . . . . . 18 (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ βˆ…) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
232230, 231eqtrdi 2789 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
233232adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
234210, 233eqtrd 2773 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
235208, 234oveq12d 7424 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))))
236235eqeq1d 2735 . . . . . . . . . . . . 13 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ ((𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = 𝑦))
237188, 236sbcied 3822 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ([(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = 𝑦))
238177, 237mpbird 257 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
239166adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)))
240239eqcomd 2739 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) = 𝑦)
241187adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
242 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
243239eleq1d 2819 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹) ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ dom β—‘(π‘Šβ€˜π‘‹)))
24418adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
245 rnss 5937 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) β†’ ran (π‘Šβ€˜π‘‹) βŠ† ran (𝑋 Γ— 𝑋))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ran (π‘Šβ€˜π‘‹) βŠ† ran (𝑋 Γ— 𝑋))
247 df-rn 5687 . . . . . . . . . . . . . . . . . . . . . . 23 ran (π‘Šβ€˜π‘‹) = dom β—‘(π‘Šβ€˜π‘‹)
248 rnxpid 6170 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 Γ— 𝑋) = 𝑋
249246, 247, 2483sstr3g 4026 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ dom β—‘(π‘Šβ€˜π‘‹) βŠ† 𝑋)
250249sseld 3981 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ dom β—‘(π‘Šβ€˜π‘‹) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
251243, 250sylbid 239 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
252242, 251mtod 197 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ 𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹))
253 ndmima 6100 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) = βˆ…)
254252, 253syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) = βˆ…)
255239sneqd 4640 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ {𝑦} = {(𝑋𝐹(π‘Šβ€˜π‘‹))})
256255imaeq2d 6058 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}) = (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
257 df-ima 5689 . . . . . . . . . . . . . . . . . . . 20 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ran (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
258 cnvxp 6154 . . . . . . . . . . . . . . . . . . . . . . . 24 β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
259258reseq1i 5976 . . . . . . . . . . . . . . . . . . . . . . 23 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = (({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
260 ssid 4004 . . . . . . . . . . . . . . . . . . . . . . . 24 {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}
261 xpssres 6017 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ (({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋))
262260, 261ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
263259, 262eqtri 2761 . . . . . . . . . . . . . . . . . . . . . 22 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
264263rneqi 5935 . . . . . . . . . . . . . . . . . . . . 21 ran (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ran ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
26546snnz 4780 . . . . . . . . . . . . . . . . . . . . . 22 {(𝑋𝐹(π‘Šβ€˜π‘‹))} β‰  βˆ…
266 rnxp 6167 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} β‰  βˆ… β†’ ran ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) = 𝑋)
267265, 266ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ran ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) = 𝑋
268264, 267eqtri 2761 . . . . . . . . . . . . . . . . . . . 20 ran (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = 𝑋
269257, 268eqtri 2761 . . . . . . . . . . . . . . . . . . 19 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = 𝑋
270256, 269eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}) = 𝑋)
271254, 270uneq12d 4164 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βˆͺ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦})) = (βˆ… βˆͺ 𝑋))
272 cnvun 6140 . . . . . . . . . . . . . . . . . . 19 β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) = (β—‘(π‘Šβ€˜π‘‹) βˆͺ β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
273272imaeq1i 6055 . . . . . . . . . . . . . . . . . 18 (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = ((β—‘(π‘Šβ€˜π‘‹) βˆͺ β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})
274 imaundir 6148 . . . . . . . . . . . . . . . . . 18 ((β—‘(π‘Šβ€˜π‘‹) βˆͺ β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βˆͺ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}))
275273, 274eqtri 2761 . . . . . . . . . . . . . . . . 17 (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βˆͺ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}))
276 un0 4390 . . . . . . . . . . . . . . . . . 18 (𝑋 βˆͺ βˆ…) = 𝑋
277 uncom 4153 . . . . . . . . . . . . . . . . . 18 (𝑋 βˆͺ βˆ…) = (βˆ… βˆͺ 𝑋)
278276, 277eqtr3i 2763 . . . . . . . . . . . . . . . . 17 𝑋 = (βˆ… βˆͺ 𝑋)
279271, 275, 2783eqtr4g 2798 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = 𝑋)
280189, 279sylan9eqr 2795 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ 𝑒 = 𝑋)
281280sqxpeqd 5708 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒 Γ— 𝑒) = (𝑋 Γ— 𝑋))
282281ineq2d 4212 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)))
283 indir 4275 . . . . . . . . . . . . . . . . . . 19 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋)))
284 df-ss 3965 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) ↔ ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
285244, 284sylib 217 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
286 incom 4201 . . . . . . . . . . . . . . . . . . . . . . 23 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
287 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋 ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ… ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
288242, 287sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑋 ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ…)
289286, 288eqtrid 2785 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋) = βˆ…)
290289xpeq2d 5706 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑋 Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋)) = (𝑋 Γ— βˆ…))
291 xpindi 5832 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋)) = ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋))
292 xp0 6155 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 Γ— βˆ…) = βˆ…
293290, 291, 2923eqtr3g 2796 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋)) = βˆ…)
294285, 293uneq12d 4164 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋))) = ((π‘Šβ€˜π‘‹) βˆͺ βˆ…))
295283, 294eqtrid 2785 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = ((π‘Šβ€˜π‘‹) βˆͺ βˆ…))
296 un0 4390 . . . . . . . . . . . . . . . . . 18 ((π‘Šβ€˜π‘‹) βˆͺ βˆ…) = (π‘Šβ€˜π‘‹)
297295, 296eqtrdi 2789 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
298297adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
299282, 298eqtrd 2773 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = (π‘Šβ€˜π‘‹))
300280, 299oveq12d 7424 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = (𝑋𝐹(π‘Šβ€˜π‘‹)))
301300eqeq1d 2735 . . . . . . . . . . . . 13 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ ((𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) = 𝑦))
302241, 301sbcied 3822 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ([(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) = 𝑦))
303240, 302mpbird 257 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
304238, 303jaodan 957 . . . . . . . . . 10 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
305135, 304sylan2b 595 . . . . . . . . 9 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
306305ralrimiva 3147 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
307175, 306jca 513 . . . . . . 7 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦))
3082, 3fpwwe2lem2 10624 . . . . . . . 8 (πœ‘ β†’ ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ↔ (((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴 ∧ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))) ∧ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
309308adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ↔ (((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴 ∧ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))) ∧ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
31034, 307, 309mpbir2and 712 . . . . . 6 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3112relopabiv 5819 . . . . . . 7 Rel π‘Š
312311releldmi 5946 . . . . . 6 ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ dom π‘Š)
313 elssuni 4941 . . . . . 6 ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ dom π‘Š β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† βˆͺ dom π‘Š)
314310, 312, 3133syl 18 . . . . 5 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† βˆͺ dom π‘Š)
315314, 7sseqtrrdi 4033 . . . 4 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋)
3161, 315sstrid 3993 . . 3 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† 𝑋)
31746snss 4789 . . 3 ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ↔ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† 𝑋)
318316, 317sylibr 233 . 2 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
319318pm2.18da 799 1 (πœ‘ β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∨ w3o 1087   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475  [wsbc 3777   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908   class class class wbr 5148  {copab 5210   Or wor 5587   Fr wfr 5628   We wwe 5630   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679  Fun wfun 6535  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-oi 9502
This theorem is referenced by:  fpwwe2  10635
  Copyright terms: Public domain W3C validator