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

Theorem fpwwe2 10586
Description: Given any function 𝐹 from well-orderings of subsets of 𝐴 to 𝐴, there is a unique well-ordered subset βŸ¨π‘‹, (π‘Šβ€˜π‘‹)⟩ which "agrees" with 𝐹 in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 9973. Theorem 1.1 of [KanamoriPincus] p. 415. (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
fpwwe2 (πœ‘ β†’ ((π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ) ↔ (π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹))))
Distinct variable groups:   𝑦,𝑒,π‘Ÿ,π‘₯,𝐹   𝑋,π‘Ÿ,𝑒,π‘₯,𝑦   πœ‘,π‘Ÿ,𝑒,π‘₯,𝑦   𝐴,π‘Ÿ,π‘₯   𝑅,π‘Ÿ,𝑒,π‘₯,𝑦   π‘Œ,π‘Ÿ,𝑒,π‘₯,𝑦   π‘Š,π‘Ÿ,𝑒,π‘₯,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑒)   𝑉(π‘₯,𝑦,𝑒,π‘Ÿ)

Proof of Theorem fpwwe2
Dummy variables 𝑀 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2.1 . . . . . . . . . . 11 π‘Š = {⟨π‘₯, π‘ŸβŸ© ∣ ((π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯)) ∧ (π‘Ÿ We π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ [(β—‘π‘Ÿ β€œ {𝑦}) / 𝑒](𝑒𝐹(π‘Ÿ ∩ (𝑒 Γ— 𝑒))) = 𝑦))}
2 fpwwe2.2 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ 𝑉)
3 fpwwe2.3 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯)) β†’ (π‘₯πΉπ‘Ÿ) ∈ 𝐴)
4 fpwwe2.4 . . . . . . . . . . 11 𝑋 = βˆͺ dom π‘Š
51, 2, 3, 4fpwwe2lem10 10583 . . . . . . . . . 10 (πœ‘ β†’ π‘Š:dom π‘ŠβŸΆπ’« (𝑋 Γ— 𝑋))
65ffund 6677 . . . . . . . . 9 (πœ‘ β†’ Fun π‘Š)
7 funbrfv2b 6905 . . . . . . . . 9 (Fun π‘Š β†’ (π‘Œπ‘Šπ‘… ↔ (π‘Œ ∈ dom π‘Š ∧ (π‘Šβ€˜π‘Œ) = 𝑅)))
86, 7syl 17 . . . . . . . 8 (πœ‘ β†’ (π‘Œπ‘Šπ‘… ↔ (π‘Œ ∈ dom π‘Š ∧ (π‘Šβ€˜π‘Œ) = 𝑅)))
98simprbda 500 . . . . . . 7 ((πœ‘ ∧ π‘Œπ‘Šπ‘…) β†’ π‘Œ ∈ dom π‘Š)
109adantrr 716 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œ ∈ dom π‘Š)
11 elssuni 4903 . . . . . . 7 (π‘Œ ∈ dom π‘Š β†’ π‘Œ βŠ† βˆͺ dom π‘Š)
1211, 4sseqtrrdi 4000 . . . . . 6 (π‘Œ ∈ dom π‘Š β†’ π‘Œ βŠ† 𝑋)
1310, 12syl 17 . . . . 5 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œ βŠ† 𝑋)
14 simpl 484 . . . . . . 7 ((𝑋 βŠ† π‘Œ ∧ (π‘Šβ€˜π‘‹) = (𝑅 ∩ (π‘Œ Γ— 𝑋))) β†’ 𝑋 βŠ† π‘Œ)
1514a1i 11 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((𝑋 βŠ† π‘Œ ∧ (π‘Šβ€˜π‘‹) = (𝑅 ∩ (π‘Œ Γ— 𝑋))) β†’ 𝑋 βŠ† π‘Œ))
16 simplrr 777 . . . . . . . . 9 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘ŒπΉπ‘…) ∈ π‘Œ)
172adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝐴 ∈ 𝑉)
1817adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝐴 ∈ 𝑉)
191, 2, 3, 4fpwwe2lem11 10584 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 ∈ dom π‘Š)
20 funfvbrb 7006 . . . . . . . . . . . . . . . . . . . 20 (Fun π‘Š β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
216, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
2219, 21mpbid 231 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
231, 2fpwwe2lem2 10575 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ↔ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
2422, 23mpbid 231 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
2524ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
2625simpld 496 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)))
2726simpld 496 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑋 βŠ† 𝐴)
2818, 27ssexd 5286 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑋 ∈ V)
2928difexd 5291 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βˆ– π‘Œ) ∈ V)
3025simprd 497 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))
3130simpld 496 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘Šβ€˜π‘‹) We 𝑋)
32 wefr 5628 . . . . . . . . . . . . 13 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
3331, 32syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
34 difssd 4097 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βˆ– π‘Œ) βŠ† 𝑋)
35 fri 5598 . . . . . . . . . . . . 13 ((((𝑋 βˆ– π‘Œ) ∈ V ∧ (π‘Šβ€˜π‘‹) Fr 𝑋) ∧ ((𝑋 βˆ– π‘Œ) βŠ† 𝑋 ∧ (𝑋 βˆ– π‘Œ) β‰  βˆ…)) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
3635expr 458 . . . . . . . . . . . 12 ((((𝑋 βˆ– π‘Œ) ∈ V ∧ (π‘Šβ€˜π‘‹) Fr 𝑋) ∧ (𝑋 βˆ– π‘Œ) βŠ† 𝑋) β†’ ((𝑋 βˆ– π‘Œ) β‰  βˆ… β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧))
3729, 33, 34, 36syl21anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 βˆ– π‘Œ) β‰  βˆ… β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧))
38 ssdif0 4328 . . . . . . . . . . . . . . 15 ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βŠ† π‘Œ ↔ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βˆ– π‘Œ) = βˆ…)
39 indif1 4236 . . . . . . . . . . . . . . . 16 ((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βˆ– π‘Œ)
4039eqeq1i 2742 . . . . . . . . . . . . . . 15 (((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = βˆ… ↔ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βˆ– π‘Œ) = βˆ…)
41 disj 4412 . . . . . . . . . . . . . . . 16 (((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = βˆ… ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
42 vex 3452 . . . . . . . . . . . . . . . . . . . 20 𝑀 ∈ V
4342eliniseg 6051 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V β†’ (𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ 𝑀(π‘Šβ€˜π‘‹)𝑧))
4443elv 3454 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4544notbii 320 . . . . . . . . . . . . . . . . 17 (Β¬ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4645ralbii 3097 . . . . . . . . . . . . . . . 16 (βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4741, 46bitri 275 . . . . . . . . . . . . . . 15 (((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = βˆ… ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4838, 40, 473bitr2i 299 . . . . . . . . . . . . . 14 ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βŠ† π‘Œ ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
49 cnvimass 6038 . . . . . . . . . . . . . . . . 17 (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† dom (π‘Šβ€˜π‘‹)
5026simprd 497 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
51 dmss 5863 . . . . . . . . . . . . . . . . . . 19 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
53 dmxpid 5890 . . . . . . . . . . . . . . . . . 18 dom (𝑋 Γ— 𝑋) = 𝑋
5452, 53sseqtrdi 3999 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ dom (π‘Šβ€˜π‘‹) βŠ† 𝑋)
5549, 54sstrid 3960 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† 𝑋)
56 sseqin2 4180 . . . . . . . . . . . . . . . 16 ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† 𝑋 ↔ (𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
5755, 56sylib 217 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
5857sseq1d 3980 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βŠ† π‘Œ ↔ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ))
5948, 58bitr3id 285 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ))
6059rexbidv 3176 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ))
61 eldifn 4092 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (𝑋 βˆ– π‘Œ) β†’ Β¬ 𝑧 ∈ π‘Œ)
6261ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ Β¬ 𝑧 ∈ π‘Œ)
63 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 = 𝑧 β†’ (𝑀 ∈ π‘Œ ↔ 𝑧 ∈ π‘Œ))
6463notbid 318 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 = 𝑧 β†’ (Β¬ 𝑀 ∈ π‘Œ ↔ Β¬ 𝑧 ∈ π‘Œ))
6562, 64syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑀 = 𝑧 β†’ Β¬ 𝑀 ∈ π‘Œ))
6665con2d 134 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑀 ∈ π‘Œ β†’ Β¬ 𝑀 = 𝑧))
6766imp 408 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ Β¬ 𝑀 = 𝑧)
6862adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ Β¬ 𝑧 ∈ π‘Œ)
69 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))
7069ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))
7170breqd 5121 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 ↔ 𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀))
72 eldifi 4091 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝑋 βˆ– π‘Œ) β†’ 𝑧 ∈ 𝑋)
7372ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑧 ∈ 𝑋)
7473adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑧 ∈ 𝑋)
75 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀 ∈ π‘Œ)
76 brxp 5686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 Γ— π‘Œ)𝑀 ↔ (𝑧 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ))
7774, 75, 76sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑧(𝑋 Γ— π‘Œ)𝑀)
78 brin 5162 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀 ↔ (𝑧(π‘Šβ€˜π‘‹)𝑀 ∧ 𝑧(𝑋 Γ— π‘Œ)𝑀))
7978rbaib 540 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 Γ— π‘Œ)𝑀 β†’ (𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑀))
8077, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑀))
8171, 80bitrd 279 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑀))
821, 2fpwwe2lem2 10575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (π‘Œπ‘Šπ‘… ↔ ((π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)) ∧ (𝑅 We π‘Œ ∧ βˆ€π‘¦ ∈ π‘Œ [(◑𝑅 β€œ {𝑦}) / 𝑒](𝑒𝐹(𝑅 ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
8382biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘Œπ‘Šπ‘…) β†’ ((π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)) ∧ (𝑅 We π‘Œ ∧ βˆ€π‘¦ ∈ π‘Œ [(◑𝑅 β€œ {𝑦}) / 𝑒](𝑒𝐹(𝑅 ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
8483adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)) ∧ (𝑅 We π‘Œ ∧ βˆ€π‘¦ ∈ π‘Œ [(◑𝑅 β€œ {𝑦}) / 𝑒](𝑒𝐹(𝑅 ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
8584simpld 496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ (π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)))
8685simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝑅 βŠ† (π‘Œ Γ— π‘Œ))
8786ad5ant12 755 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑅 βŠ† (π‘Œ Γ— π‘Œ))
8887ssbrd 5153 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 β†’ 𝑧(π‘Œ Γ— π‘Œ)𝑀))
89 brxp 5686 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(π‘Œ Γ— π‘Œ)𝑀 ↔ (𝑧 ∈ π‘Œ ∧ 𝑀 ∈ π‘Œ))
9089simplbi 499 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧(π‘Œ Γ— π‘Œ)𝑀 β†’ 𝑧 ∈ π‘Œ)
9188, 90syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 β†’ 𝑧 ∈ π‘Œ))
9281, 91sylbird 260 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧(π‘Šβ€˜π‘‹)𝑀 β†’ 𝑧 ∈ π‘Œ))
9368, 92mtod 197 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀)
9431ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (π‘Šβ€˜π‘‹) We 𝑋)
95 weso 5629 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
9713ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘Œ βŠ† 𝑋)
9897sselda 3949 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀 ∈ 𝑋)
99 sotric 5578 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Šβ€˜π‘‹) Or 𝑋 ∧ (𝑀 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ Β¬ (𝑀 = 𝑧 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑀)))
100 ioran 983 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ (𝑀 = 𝑧 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑀) ↔ (Β¬ 𝑀 = 𝑧 ∧ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀))
10199, 100bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Šβ€˜π‘‹) Or 𝑋 ∧ (𝑀 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ (Β¬ 𝑀 = 𝑧 ∧ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀)))
10296, 98, 74, 101syl12anc 836 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ (Β¬ 𝑀 = 𝑧 ∧ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀)))
10367, 93, 102mpbir2and 712 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀(π‘Šβ€˜π‘‹)𝑧)
104103, 44sylibr 233 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
105104ex 414 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑀 ∈ π‘Œ β†’ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))
106105ssrdv 3955 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘Œ βŠ† (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
107 simprr 772 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)
108106, 107eqssd 3966 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘Œ = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
109 in32 4186 . . . . . . . . . . . . . . . . . 18 (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)) ∩ (π‘Œ Γ— π‘Œ)) = (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) ∩ (𝑋 Γ— π‘Œ))
110 simplrr 777 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))
111110ineq1d 4176 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑅 ∩ (π‘Œ Γ— π‘Œ)) = (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)) ∩ (π‘Œ Γ— π‘Œ)))
11286ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 βŠ† (π‘Œ Γ— π‘Œ))
113 df-ss 3932 . . . . . . . . . . . . . . . . . . . 20 (𝑅 βŠ† (π‘Œ Γ— π‘Œ) ↔ (𝑅 ∩ (π‘Œ Γ— π‘Œ)) = 𝑅)
114112, 113sylib 217 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑅 ∩ (π‘Œ Γ— π‘Œ)) = 𝑅)
115111, 114eqtr3d 2779 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)) ∩ (π‘Œ Γ— π‘Œ)) = 𝑅)
116 inss2 4194 . . . . . . . . . . . . . . . . . . . 20 ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) βŠ† (π‘Œ Γ— π‘Œ)
117 xpss1 5657 . . . . . . . . . . . . . . . . . . . . 21 (π‘Œ βŠ† 𝑋 β†’ (π‘Œ Γ— π‘Œ) βŠ† (𝑋 Γ— π‘Œ))
11897, 117syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘Œ Γ— π‘Œ) βŠ† (𝑋 Γ— π‘Œ))
119116, 118sstrid 3960 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) βŠ† (𝑋 Γ— π‘Œ))
120 df-ss 3932 . . . . . . . . . . . . . . . . . . 19 (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) βŠ† (𝑋 Γ— π‘Œ) ↔ (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) ∩ (𝑋 Γ— π‘Œ)) = ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)))
121119, 120sylib 217 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) ∩ (𝑋 Γ— π‘Œ)) = ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)))
122109, 115, 1213eqtr3a 2801 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)))
123108sqxpeqd 5670 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘Œ Γ— π‘Œ) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))
124123ineq2d 4177 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))))
125122, 124eqtrd 2777 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))))
126108, 125oveq12d 7380 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘ŒπΉπ‘…) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))))
12718adantr 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝐴 ∈ 𝑉)
12822adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
129128ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
1301, 127, 129fpwwe2lem3 10576 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑧 ∈ 𝑋) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))) = 𝑧)
13173, 130mpdan 686 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))) = 𝑧)
132126, 131eqtrd 2777 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘ŒπΉπ‘…) = 𝑧)
133132, 62eqneltrd 2858 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ)
134133rexlimdvaa 3154 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ))
13560, 134sylbid 239 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧 β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ))
13637, 135syld 47 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 βˆ– π‘Œ) β‰  βˆ… β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ))
137136necon4ad 2963 . . . . . . . . 9 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((π‘ŒπΉπ‘…) ∈ π‘Œ β†’ (𝑋 βˆ– π‘Œ) = βˆ…))
13816, 137mpd 15 . . . . . . . 8 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βˆ– π‘Œ) = βˆ…)
139 ssdif0 4328 . . . . . . . 8 (𝑋 βŠ† π‘Œ ↔ (𝑋 βˆ– π‘Œ) = βˆ…)
140138, 139sylibr 233 . . . . . . 7 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑋 βŠ† π‘Œ)
141140ex 414 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))) β†’ 𝑋 βŠ† π‘Œ))
1423adantlr 714 . . . . . . 7 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯)) β†’ (π‘₯πΉπ‘Ÿ) ∈ 𝐴)
143 simprl 770 . . . . . . 7 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œπ‘Šπ‘…)
1441, 17, 142, 128, 143fpwwe2lem9 10582 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((𝑋 βŠ† π‘Œ ∧ (π‘Šβ€˜π‘‹) = (𝑅 ∩ (π‘Œ Γ— 𝑋))) ∨ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))))
14515, 141, 144mpjaod 859 . . . . 5 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝑋 βŠ† π‘Œ)
14613, 145eqssd 3966 . . . 4 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œ = 𝑋)
1476adantr 482 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ Fun π‘Š)
148146, 143eqbrtrrd 5134 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘‹π‘Šπ‘…)
149 funbrfv 6898 . . . . . 6 (Fun π‘Š β†’ (π‘‹π‘Šπ‘… β†’ (π‘Šβ€˜π‘‹) = 𝑅))
150147, 148, 149sylc 65 . . . . 5 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ (π‘Šβ€˜π‘‹) = 𝑅)
151150eqcomd 2743 . . . 4 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝑅 = (π‘Šβ€˜π‘‹))
152146, 151jca 513 . . 3 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ (π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)))
153152ex 414 . 2 (πœ‘ β†’ ((π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ) β†’ (π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹))))
1541, 2, 3, 4fpwwe2lem12 10585 . . . 4 (πœ‘ β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
15522, 154jca 513 . . 3 (πœ‘ β†’ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
156 breq12 5115 . . . 4 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ (π‘Œπ‘Šπ‘… ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
157 oveq12 7371 . . . . 5 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ (π‘ŒπΉπ‘…) = (𝑋𝐹(π‘Šβ€˜π‘‹)))
158 simpl 484 . . . . 5 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ π‘Œ = 𝑋)
159157, 158eleq12d 2832 . . . 4 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ ((π‘ŒπΉπ‘…) ∈ π‘Œ ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
160156, 159anbi12d 632 . . 3 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ ((π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ) ↔ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)))
161155, 160syl5ibrcom 247 . 2 (πœ‘ β†’ ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)))
162153, 161impbid 211 1 (πœ‘ β†’ ((π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ) ↔ (π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448  [wsbc 3744   βˆ– cdif 3912   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  π’« cpw 4565  {csn 4591  βˆͺ cuni 4870   class class class wbr 5110  {copab 5172   Or wor 5549   Fr wfr 5590   We wwe 5592   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638   β€œ cima 5641  Fun wfun 6495  β€˜cfv 6501  (class class class)co 7362
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-oi 9453
This theorem is referenced by:  fpwwe  10589  canthwelem  10593  pwfseqlem4  10605
  Copyright terms: Public domain W3C validator