MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2lem12 Structured version   Visualization version   GIF version
Theorem fpwwe2lem12 10633
Description: Lemma for fpwwe2 10634. (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 4165 . . . 4 {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
2 fpwwe2.1 . . . . . . . . . . . . . 14 π‘Š = {⟨π‘₯, π‘ŸβŸ© ∣ ((π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯)) ∧ (π‘Ÿ We π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ [(β—‘π‘Ÿ β€œ {𝑦}) / 𝑒](𝑒𝐹(π‘Ÿ ∩ (𝑒 Γ— 𝑒))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 ∈ 𝑉)
43adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝐴 ∈ 𝑉)
5 fpwwe2.3 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯)) β†’ (π‘₯πΉπ‘Ÿ) ∈ 𝐴)
65adantlr 712 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯)) β†’ (π‘₯πΉπ‘Ÿ) ∈ 𝐴)
7 fpwwe2.4 . . . . . . . . . . . . . 14 𝑋 = βˆͺ dom π‘Š
82, 4, 6, 7fpwwe2lem11 10632 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝑋 ∈ dom π‘Š)
92, 4, 6, 7fpwwe2lem10 10631 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ π‘Š:dom π‘ŠβŸΆπ’« (𝑋 Γ— 𝑋))
10 ffun 6710 . . . . . . . . . . . . . 14 (π‘Š:dom π‘ŠβŸΆπ’« (𝑋 Γ— 𝑋) β†’ Fun π‘Š)
11 funfvbrb 7042 . . . . . . . . . . . . . 14 (Fun π‘Š β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
129, 10, 113syl 18 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
138, 12mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
142, 4fpwwe2lem2 10623 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ↔ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
1513, 14mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
1615simpld 494 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)))
1716simpld 494 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝑋 βŠ† 𝐴)
1816simprd 495 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
1915simprd 495 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))
2019simpld 494 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) We 𝑋)
2117, 18, 203jca 1125 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) ∧ (π‘Šβ€˜π‘‹) We 𝑋))
222, 3, 5fpwwe2lem4 10625 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) ∧ (π‘Šβ€˜π‘‹) We 𝑋)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝐴)
2321, 22syldan 590 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝐴)
2423snssd 4804 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† 𝐴)
2517, 24unssd 4178 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴)
26 ssun1 4164 . . . . . . . . . . 11 𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
27 xpss12 5681 . . . . . . . . . . 11 ((𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑋 Γ— 𝑋) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
2826, 26, 27mp2an 689 . . . . . . . . . 10 (𝑋 Γ— 𝑋) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
2918, 28sstrdi 3986 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
30 xpss12 5681 . . . . . . . . . . 11 ((𝑋 βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3126, 1, 30mp2an 689 . . . . . . . . . 10 (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
3231a1i 11 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3329, 32unssd 4178 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3425, 33jca 511 . . . . . . 7 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴 ∧ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))))
35 ssdif0 4355 . . . . . . . . . . . . . 14 (π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} ↔ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ…)
36 simpllr 773 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
3718ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
3837ssbrd 5181 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)(𝑋𝐹(π‘Šβ€˜π‘‹))))
39 brxp 5715 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)(𝑋𝐹(π‘Šβ€˜π‘‹)) ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
4039simplbi 497 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
4138, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
4236, 41mtod 197 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)))
43 brxp 5715 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)) ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
4443simplbi 497 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
4536, 44nsyl 140 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)))
46 ovex 7434 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ V
47 breq2 5142 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))(𝑋𝐹(π‘Šβ€˜π‘‹))))
48 brun 5189 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))(𝑋𝐹(π‘Šβ€˜π‘‹)) ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
4947, 48bitrdi 287 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)))))
5049notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹)))))
5146, 50rexsn 4678 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
52 ioran 980 . . . . . . . . . . . . . . . . . 18 (Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))) ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
5351, 52bitri 275 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)(𝑋𝐹(π‘Šβ€˜π‘‹)) ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})(𝑋𝐹(π‘Šβ€˜π‘‹))))
5442, 45, 53sylanbrc 582 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
55 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))})
56 sssn 4821 . . . . . . . . . . . . . . . . . . 19 (π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} ↔ (π‘₯ = βˆ… ∨ π‘₯ = {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
5755, 56sylib 217 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯ = βˆ… ∨ π‘₯ = {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
58 simplrr 775 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ β‰  βˆ…)
5958neneqd 2937 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ π‘₯ = βˆ…)
6057, 59orcnd 875 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ = {(𝑋𝐹(π‘Šβ€˜π‘‹))})
6160raleqdv 3317 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
62 breq1 5141 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6362notbid 318 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6446, 63ralsn 4677 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
6561, 64bitrdi 287 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6660, 65rexeqbidv 3335 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ βˆƒπ‘¦ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6754, 66mpbird 257 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
6867ex 412 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ (π‘₯ βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
6935, 68biimtrrid 242 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ… β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
70 vex 3470 . . . . . . . . . . . . . . . . 17 π‘₯ ∈ V
71 difexg 5317 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ V β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
7270, 71mp1i 13 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
73 wefr 5656 . . . . . . . . . . . . . . . . . 18 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
7420, 73syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
7574ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
76 simplrl 774 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
77 uncom 4145 . . . . . . . . . . . . . . . . . 18 (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βˆͺ 𝑋)
7876, 77sseqtrdi 4024 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ π‘₯ βŠ† ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βˆͺ 𝑋))
79 ssundif 4479 . . . . . . . . . . . . . . . . 17 (π‘₯ βŠ† ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βˆͺ 𝑋) ↔ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋)
8078, 79sylib 217 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋)
81 simpr 484 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…)
82 fri 5626 . . . . . . . . . . . . . . . 16 ((((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V ∧ (π‘Šβ€˜π‘‹) Fr 𝑋) ∧ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋 ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…)) β†’ βˆƒπ‘¦ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦)
8372, 75, 80, 81, 82syl22anc 836 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦)
84 brun 5189 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (𝑧(π‘Šβ€˜π‘‹)𝑦 ∨ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
85 idd 24 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
86 brxp 5715 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ↔ (𝑧 ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
8786simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
88 eldifn 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
8988adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
9089pm2.21d 121 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9187, 90syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9285, 91jaod 856 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ ((𝑧(π‘Šβ€˜π‘‹)𝑦 ∨ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦) β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9384, 92biimtrid 241 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 β†’ 𝑧(π‘Šβ€˜π‘‹)𝑦))
9493con3d 152 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
9594ralimdv 3161 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
96 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
9796ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
9818ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
9998ssbrd 5181 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 β†’ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)𝑦))
100 brxp 5715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))
101100simplbi 497 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— 𝑋)𝑦 β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
10299, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
10397, 102mtod 197 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦)
104 brxp 5715 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
105104simprbi 496 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
10689, 105nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)
107 brun 5189 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐹(π‘Šβ€˜π‘‹))((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
10862, 107bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)))
109108notbid 318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ (Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)))
11046, 109ralsn 4677 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
111 ioran 980 . . . . . . . . . . . . . . . . . . . . . 22 (Β¬ ((𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∨ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦) ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
112110, 111bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ (Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(π‘Šβ€˜π‘‹)𝑦 ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹))(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
113103, 106, 112sylanbrc 582 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
11495, 113jctird 526 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∧ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)))
115 ssun1 4164 . . . . . . . . . . . . . . . . . . . . 21 π‘₯ βŠ† (π‘₯ βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
116 undif1 4467 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = (π‘₯ βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
117115, 116sseqtrri 4011 . . . . . . . . . . . . . . . . . . . 20 π‘₯ βŠ† ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
118 ralun 4184 . . . . . . . . . . . . . . . . . . . 20 ((βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∧ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦) β†’ βˆ€π‘§ ∈ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
119 ssralv 4042 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ βŠ† ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (βˆ€π‘§ ∈ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 β†’ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
120117, 118, 119mpsyl 68 . . . . . . . . . . . . . . . . . . 19 ((βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∧ βˆ€π‘§ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦) β†’ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
121114, 120syl6 35 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
122 eldifi 4118 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ 𝑦 ∈ π‘₯)
123122adantl 481 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ 𝑦 ∈ π‘₯)
124121, 123jctild 525 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) ∧ 𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ (𝑦 ∈ π‘₯ ∧ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)))
125124expimpd 453 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ ((𝑦 ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦) β†’ (𝑦 ∈ π‘₯ ∧ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)))
126125reximdv2 3156 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ (βˆƒπ‘¦ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘§ ∈ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑦 β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
12783, 126mpd 15 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) ∧ (π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
128127ex 412 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ ((π‘₯ βˆ– {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β‰  βˆ… β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
12969, 128pm2.61dne 3020 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…)) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
130129ex 412 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
131130alrimiv 1922 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ βˆ€π‘₯((π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
132 df-fr 5621 . . . . . . . . . 10 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) Fr (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ βˆ€π‘₯((π‘₯ βŠ† (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ Β¬ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
133131, 132sylibr 233 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) Fr (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
134 elun 4140 . . . . . . . . . . . 12 (π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ (π‘₯ ∈ 𝑋 ∨ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
135 elun 4140 . . . . . . . . . . . 12 (𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
136134, 135anbi12i 626 . . . . . . . . . . 11 ((π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ↔ ((π‘₯ ∈ 𝑋 ∨ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
137 weso 5657 . . . . . . . . . . . . . . . 16 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
13820, 137syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
139 solin 5603 . . . . . . . . . . . . . . 15 (((π‘Šβ€˜π‘‹) Or 𝑋 ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯(π‘Šβ€˜π‘‹)𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦(π‘Šβ€˜π‘‹)π‘₯))
140138, 139sylan 579 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯(π‘Šβ€˜π‘‹)𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦(π‘Šβ€˜π‘‹)π‘₯))
141 ssun1 4164 . . . . . . . . . . . . . . . . 17 (π‘Šβ€˜π‘‹) βŠ† ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
142141a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Šβ€˜π‘‹) βŠ† ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
143142ssbrd 5181 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯(π‘Šβ€˜π‘‹)𝑦 β†’ π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
144 idd 24 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯ = 𝑦 β†’ π‘₯ = 𝑦))
145142ssbrd 5181 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦(π‘Šβ€˜π‘‹)π‘₯ β†’ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
146143, 144, 1453orim123d 1440 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘₯(π‘Šβ€˜π‘‹)𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦(π‘Šβ€˜π‘‹)π‘₯) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
147140, 146mpd 15 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
148147ex 412 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
149 simpr 484 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋))
150149ancomd 461 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦 ∈ 𝑋 ∧ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
151 brxp 5715 . . . . . . . . . . . . . . 15 (𝑦(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘₯ ↔ (𝑦 ∈ 𝑋 ∧ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
152150, 151sylibr 233 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ 𝑦(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘₯)
153 ssun2 4165 . . . . . . . . . . . . . . 15 (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
154153ssbri 5183 . . . . . . . . . . . . . 14 (𝑦(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘₯ β†’ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)
155 3mix3 1329 . . . . . . . . . . . . . 14 (𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯ β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
156152, 154, 1553syl 18 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋)) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
157156ex 412 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
158 simpr 484 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
159 brxp 5715 . . . . . . . . . . . . . . 15 (π‘₯(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ↔ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
160158, 159sylibr 233 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ π‘₯(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)
161153ssbri 5183 . . . . . . . . . . . . . 14 (π‘₯(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
162 3mix1 1327 . . . . . . . . . . . . . 14 (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
163160, 161, 1623syl 18 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
164163ex 412 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
165 elsni 4637 . . . . . . . . . . . . . . 15 (π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ π‘₯ = (𝑋𝐹(π‘Šβ€˜π‘‹)))
166 elsni 4637 . . . . . . . . . . . . . . 15 (𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)))
167 eqtr3 2750 . . . . . . . . . . . . . . 15 ((π‘₯ = (𝑋𝐹(π‘Šβ€˜π‘‹)) ∧ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹))) β†’ π‘₯ = 𝑦)
168165, 166, 167syl2an 595 . . . . . . . . . . . . . 14 ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ π‘₯ = 𝑦)
1691683mix2d 1334 . . . . . . . . . . . . 13 ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
170169a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
171148, 157, 164, 170ccased 1035 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (((π‘₯ ∈ 𝑋 ∨ π‘₯ ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
172136, 171biimtrid 241 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
173172ralrimivv 3190 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ βˆ€π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})(π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯))
174 dfwe2 7754 . . . . . . . . 9 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ↔ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) Fr (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})(π‘₯((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))π‘₯)))
175133, 173, 174sylanbrc 582 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
1762fpwwe2cbv 10621 . . . . . . . . . . . . 13 π‘Š = {βŸ¨π‘Ž, π‘ βŸ© ∣ ((π‘Ž βŠ† 𝐴 ∧ 𝑠 βŠ† (π‘Ž Γ— π‘Ž)) ∧ (𝑠 We π‘Ž ∧ βˆ€π‘§ ∈ π‘Ž [(◑𝑠 β€œ {𝑧}) / 𝑏](𝑏𝐹(𝑠 ∩ (𝑏 Γ— 𝑏))) = 𝑧))}
177176, 4, 13fpwwe2lem3 10624 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = 𝑦)
178 cnvimass 6070 . . . . . . . . . . . . . . 15 (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) βŠ† dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
179 fvex 6894 . . . . . . . . . . . . . . . . 17 (π‘Šβ€˜π‘‹) ∈ V
180 snex 5421 . . . . . . . . . . . . . . . . . 18 {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∈ V
181 xpexg 7730 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ dom π‘Š ∧ {(𝑋𝐹(π‘Šβ€˜π‘‹))} ∈ V) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
1828, 180, 181sylancl 585 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V)
183 unexg 7729 . . . . . . . . . . . . . . . . 17 (((π‘Šβ€˜π‘‹) ∈ V ∧ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ V) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V)
184179, 182, 183sylancr 586 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V)
185184dmexd 7889 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V)
186 ssexg 5313 . . . . . . . . . . . . . . 15 (((β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) βŠ† dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∧ dom ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∈ V) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
187178, 185, 186sylancr 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
188187adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
189 id 22 . . . . . . . . . . . . . . . 16 (𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) β†’ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}))
190 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ 𝑦 ∈ 𝑋)
191 simplr 766 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
192 nelne2 3032 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ 𝑋 ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ 𝑦 β‰  (𝑋𝐹(π‘Šβ€˜π‘‹)))
193190, 191, 192syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ 𝑦 β‰  (𝑋𝐹(π‘Šβ€˜π‘‹)))
19487, 166syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)))
195194necon3ai 2957 . . . . . . . . . . . . . . . . . . . 20 (𝑦 β‰  (𝑋𝐹(π‘Šβ€˜π‘‹)) β†’ Β¬ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦)
196 biorf 933 . . . . . . . . . . . . . . . . . . . 20 (Β¬ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 β†’ (𝑧(π‘Šβ€˜π‘‹)𝑦 ↔ (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦)))
197193, 195, 1963syl 18 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (𝑧(π‘Šβ€˜π‘‹)𝑦 ↔ (𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦)))
198 orcom 867 . . . . . . . . . . . . . . . . . . . 20 ((𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦) ↔ (𝑧(π‘Šβ€˜π‘‹)𝑦 ∨ 𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦))
199198, 84bitr4i 278 . . . . . . . . . . . . . . . . . . 19 ((𝑧(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})𝑦 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑦) ↔ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
200197, 199bitr2di 288 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑦))
201 vex 3470 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
202201eliniseg 6083 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V β†’ (𝑧 ∈ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ↔ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦))
203202elv 3472 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ↔ 𝑧((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))𝑦)
204201eliniseg 6083 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V β†’ (𝑧 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ↔ 𝑧(π‘Šβ€˜π‘‹)𝑦))
205204elv 3472 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ↔ 𝑧(π‘Šβ€˜π‘‹)𝑦)
206200, 203, 2053bitr4g 314 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (𝑧 ∈ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ↔ 𝑧 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
207206eqrdv 2722 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
208189, 207sylan9eqr 2786 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ 𝑒 = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
209208sqxpeqd 5698 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒 Γ— 𝑒) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
210209ineq2d 4204 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
211 indir 4267 . . . . . . . . . . . . . . . . . . 19 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
212 inxp 5822 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
213 incom 4193 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
214 cnvimass 6070 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βŠ† dom (π‘Šβ€˜π‘‹)
21518adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
216 dmss 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
217215, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
218 dmxpid 5919 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑋 Γ— 𝑋) = 𝑋
219217, 218sseqtrdi 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† 𝑋)
220214, 219sstrid 3985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βŠ† 𝑋)
221220, 191ssneldd 3977 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
222 disjsn 4707 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ… ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))
223221, 222sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ…)
224213, 223eqtrid 2776 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) = βˆ…)
225224xpeq2d 5696 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— βˆ…))
226 xp0 6147 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— βˆ…) = βˆ…
227225, 226eqtrdi 2780 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})) Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = βˆ…)
228212, 227eqtrid 2776 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = βˆ…)
229228uneq2d 4155 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ βˆ…))
230211, 229eqtrid 2776 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ βˆ…))
231 un0 4382 . . . . . . . . . . . . . . . . . 18 (((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) βˆͺ βˆ…) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))
232230, 231eqtrdi 2780 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
233232adantr 480 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
234210, 233eqtrd 2764 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}))))
235208, 234oveq12d 7419 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))))
236235eqeq1d 2726 . . . . . . . . . . . . 13 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ ((𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = 𝑦))
237188, 236sbcied 3814 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ ([(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦})))) = 𝑦))
238177, 237mpbird 257 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
239166adantl 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ 𝑦 = (𝑋𝐹(π‘Šβ€˜π‘‹)))
240239eqcomd 2730 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) = 𝑦)
241187adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) ∈ V)
242 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
243239eleq1d 2810 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹) ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ dom β—‘(π‘Šβ€˜π‘‹)))
24418adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
245 rnss 5928 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) β†’ ran (π‘Šβ€˜π‘‹) βŠ† ran (𝑋 Γ— 𝑋))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ran (π‘Šβ€˜π‘‹) βŠ† ran (𝑋 Γ— 𝑋))
247 df-rn 5677 . . . . . . . . . . . . . . . . . . . . . . 23 ran (π‘Šβ€˜π‘‹) = dom β—‘(π‘Šβ€˜π‘‹)
248 rnxpid 6162 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 Γ— 𝑋) = 𝑋
249246, 247, 2483sstr3g 4018 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ dom β—‘(π‘Šβ€˜π‘‹) βŠ† 𝑋)
250249sseld 3973 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ dom β—‘(π‘Šβ€˜π‘‹) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
251243, 250sylbid 239 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
252242, 251mtod 197 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ Β¬ 𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹))
253 ndmima 6092 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑦 ∈ dom β—‘(π‘Šβ€˜π‘‹) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) = βˆ…)
254252, 253syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) = βˆ…)
255239sneqd 4632 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ {𝑦} = {(𝑋𝐹(π‘Šβ€˜π‘‹))})
256255imaeq2d 6049 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}) = (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
257 df-ima 5679 . . . . . . . . . . . . . . . . . . . 20 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ran (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
258 cnvxp 6146 . . . . . . . . . . . . . . . . . . . . . . . 24 β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
259258reseq1i 5967 . . . . . . . . . . . . . . . . . . . . . . 23 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = (({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
260 ssid 3996 . . . . . . . . . . . . . . . . . . . . . . . 24 {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))}
261 xpssres 6008 . . . . . . . . . . . . . . . . . . . . . . . 24 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† {(𝑋𝐹(π‘Šβ€˜π‘‹))} β†’ (({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋))
262260, 261ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
263259, 262eqtri 2752 . . . . . . . . . . . . . . . . . . . . . 22 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
264263rneqi 5926 . . . . . . . . . . . . . . . . . . . . 21 ran (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = ran ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋)
26546snnz 4772 . . . . . . . . . . . . . . . . . . . . . 22 {(𝑋𝐹(π‘Šβ€˜π‘‹))} β‰  βˆ…
266 rnxp 6159 . . . . . . . . . . . . . . . . . . . . . 22 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} β‰  βˆ… β†’ ran ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) = 𝑋)
267265, 266ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ran ({(𝑋𝐹(π‘Šβ€˜π‘‹))} Γ— 𝑋) = 𝑋
268264, 267eqtri 2752 . . . . . . . . . . . . . . . . . . . 20 ran (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†Ύ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = 𝑋
269257, 268eqtri 2752 . . . . . . . . . . . . . . . . . . 19 (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = 𝑋
270256, 269eqtrdi 2780 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}) = 𝑋)
271254, 270uneq12d 4156 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βˆͺ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦})) = (βˆ… βˆͺ 𝑋))
272 cnvun 6132 . . . . . . . . . . . . . . . . . . 19 β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) = (β—‘(π‘Šβ€˜π‘‹) βˆͺ β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}))
273272imaeq1i 6046 . . . . . . . . . . . . . . . . . 18 (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = ((β—‘(π‘Šβ€˜π‘‹) βˆͺ β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})
274 imaundir 6140 . . . . . . . . . . . . . . . . . 18 ((β—‘(π‘Šβ€˜π‘‹) βˆͺ β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βˆͺ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}))
275273, 274eqtri 2752 . . . . . . . . . . . . . . . . 17 (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) βˆͺ (β—‘(𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β€œ {𝑦}))
276 un0 4382 . . . . . . . . . . . . . . . . . 18 (𝑋 βˆͺ βˆ…) = 𝑋
277 uncom 4145 . . . . . . . . . . . . . . . . . 18 (𝑋 βˆͺ βˆ…) = (βˆ… βˆͺ 𝑋)
278276, 277eqtr3i 2754 . . . . . . . . . . . . . . . . 17 𝑋 = (βˆ… βˆͺ 𝑋)
279271, 275, 2783eqtr4g 2789 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) = 𝑋)
280189, 279sylan9eqr 2786 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ 𝑒 = 𝑋)
281280sqxpeqd 5698 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒 Γ— 𝑒) = (𝑋 Γ— 𝑋))
282281ineq2d 4204 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)))
283 indir 4267 . . . . . . . . . . . . . . . . . . 19 (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋)))
284 df-ss 3957 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) ↔ ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
285244, 284sylib 217 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
286 incom 4193 . . . . . . . . . . . . . . . . . . . . . . 23 ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋) = (𝑋 ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))})
287 disjsn 4707 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋 ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ… ↔ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
288242, 287sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑋 ∩ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) = βˆ…)
289286, 288eqtrid 2776 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋) = βˆ…)
290289xpeq2d 5696 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (𝑋 Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋)) = (𝑋 Γ— βˆ…))
291 xpindi 5823 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 Γ— ({(𝑋𝐹(π‘Šβ€˜π‘‹))} ∩ 𝑋)) = ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋))
292 xp0 6147 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 Γ— βˆ…) = βˆ…
293290, 291, 2923eqtr3g 2787 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋)) = βˆ…)
294285, 293uneq12d 4156 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— 𝑋)) βˆͺ ((𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∩ (𝑋 Γ— 𝑋))) = ((π‘Šβ€˜π‘‹) βˆͺ βˆ…))
295283, 294eqtrid 2776 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = ((π‘Šβ€˜π‘‹) βˆͺ βˆ…))
296 un0 4382 . . . . . . . . . . . . . . . . . 18 ((π‘Šβ€˜π‘‹) βˆͺ βˆ…) = (π‘Šβ€˜π‘‹)
297295, 296eqtrdi 2780 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
298297adantr 480 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑋 Γ— 𝑋)) = (π‘Šβ€˜π‘‹))
299282, 298eqtrd 2764 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒)) = (π‘Šβ€˜π‘‹))
300280, 299oveq12d 7419 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ (𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = (𝑋𝐹(π‘Šβ€˜π‘‹)))
301300eqeq1d 2726 . . . . . . . . . . . . 13 ((((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ 𝑒 = (β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦})) β†’ ((𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) = 𝑦))
302241, 301sbcied 3814 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ ([(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦 ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) = 𝑦))
303240, 302mpbird 257 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
304238, 303jaodan 954 . . . . . . . . . 10 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∨ 𝑦 ∈ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
305135, 304sylan2b 593 . . . . . . . . 9 (((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) ∧ 𝑦 ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ [(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
306305ralrimiva 3138 . . . . . . . 8 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦)
307175, 306jca 511 . . . . . . 7 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦))
3082, 3fpwwe2lem2 10623 . . . . . . . 8 (πœ‘ β†’ ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ↔ (((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴 ∧ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))) ∧ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
309308adantr 480 . . . . . . 7 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ↔ (((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝐴 ∧ ((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) βŠ† ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) Γ— (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}))) ∧ (((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) We (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∧ βˆ€π‘¦ ∈ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})[(β—‘((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β€œ {𝑦}) / 𝑒](𝑒𝐹(((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
31034, 307, 309mpbir2and 710 . . . . . 6 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})))
3112relopabiv 5810 . . . . . . 7 Rel π‘Š
312311releldmi 5937 . . . . . 6 ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))})π‘Š((π‘Šβ€˜π‘‹) βˆͺ (𝑋 Γ— {(𝑋𝐹(π‘Šβ€˜π‘‹))})) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ dom π‘Š)
313 elssuni 4931 . . . . . 6 ((𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) ∈ dom π‘Š β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† βˆͺ dom π‘Š)
314310, 312, 3133syl 18 . . . . 5 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† βˆͺ dom π‘Š)
315314, 7sseqtrrdi 4025 . . . 4 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋 βˆͺ {(𝑋𝐹(π‘Šβ€˜π‘‹))}) βŠ† 𝑋)
3161, 315sstrid 3985 . . 3 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† 𝑋)
31746snss 4781 . . 3 ((𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋 ↔ {(𝑋𝐹(π‘Šβ€˜π‘‹))} βŠ† 𝑋)
318316, 317sylibr 233 . 2 ((πœ‘ ∧ Β¬ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋) β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
319318pm2.18da 797 1 (πœ‘ β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∨ w3o 1083   ∧ w3a 1084  βˆ€wal 1531   = wceq 1533   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  Vcvv 3466  [wsbc 3769   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  π’« cpw 4594  {csn 4620  βˆͺ cuni 4899   class class class wbr 5138  {copab 5200   Or wor 5577   Fr wfr 5618   We wwe 5620   Γ— cxp 5664  β—‘ccnv 5665  dom cdm 5666  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669  Fun wfun 6527  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-oi 9501
This theorem is referenced by:  fpwwe2  10634
  Copyright terms: Public domain W3C validator