MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2 Structured version   Visualization version   GIF version
Theorem fpwwe2 10634
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 10021. 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 10631 . . . . . . . . . 10 (πœ‘ β†’ π‘Š:dom π‘ŠβŸΆπ’« (𝑋 Γ— 𝑋))
65ffund 6718 . . . . . . . . 9 (πœ‘ β†’ Fun π‘Š)
7 funbrfv2b 6946 . . . . . . . . 9 (Fun π‘Š β†’ (π‘Œπ‘Šπ‘… ↔ (π‘Œ ∈ dom π‘Š ∧ (π‘Šβ€˜π‘Œ) = 𝑅)))
86, 7syl 17 . . . . . . . 8 (πœ‘ β†’ (π‘Œπ‘Šπ‘… ↔ (π‘Œ ∈ dom π‘Š ∧ (π‘Šβ€˜π‘Œ) = 𝑅)))
98simprbda 499 . . . . . . 7 ((πœ‘ ∧ π‘Œπ‘Šπ‘…) β†’ π‘Œ ∈ dom π‘Š)
109adantrr 715 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œ ∈ dom π‘Š)
11 elssuni 4940 . . . . . . 7 (π‘Œ ∈ dom π‘Š β†’ π‘Œ βŠ† βˆͺ dom π‘Š)
1211, 4sseqtrrdi 4032 . . . . . 6 (π‘Œ ∈ dom π‘Š β†’ π‘Œ βŠ† 𝑋)
1310, 12syl 17 . . . . 5 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œ βŠ† 𝑋)
14 simpl 483 . . . . . . 7 ((𝑋 βŠ† π‘Œ ∧ (π‘Šβ€˜π‘‹) = (𝑅 ∩ (π‘Œ Γ— 𝑋))) β†’ 𝑋 βŠ† π‘Œ)
1514a1i 11 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((𝑋 βŠ† π‘Œ ∧ (π‘Šβ€˜π‘‹) = (𝑅 ∩ (π‘Œ Γ— 𝑋))) β†’ 𝑋 βŠ† π‘Œ))
16 simplrr 776 . . . . . . . . 9 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘ŒπΉπ‘…) ∈ π‘Œ)
172adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝐴 ∈ 𝑉)
1817adantr 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝐴 ∈ 𝑉)
191, 2, 3, 4fpwwe2lem11 10632 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 ∈ dom π‘Š)
20 funfvbrb 7049 . . . . . . . . . . . . . . . . . . . 20 (Fun π‘Š β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
216, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑋 ∈ dom π‘Š ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
2219, 21mpbid 231 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
231, 2fpwwe2lem2 10623 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ↔ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
2422, 23mpbid 231 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
2524ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)) ∧ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
2625simpld 495 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βŠ† 𝐴 ∧ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋)))
2726simpld 495 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑋 βŠ† 𝐴)
2818, 27ssexd 5323 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑋 ∈ V)
2928difexd 5328 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βˆ– π‘Œ) ∈ V)
3025simprd 496 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((π‘Šβ€˜π‘‹) We 𝑋 ∧ βˆ€π‘¦ ∈ 𝑋 [(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑦}) / 𝑒](𝑒𝐹((π‘Šβ€˜π‘‹) ∩ (𝑒 Γ— 𝑒))) = 𝑦))
3130simpld 495 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘Šβ€˜π‘‹) We 𝑋)
32 wefr 5665 . . . . . . . . . . . . 13 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
3331, 32syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘Šβ€˜π‘‹) Fr 𝑋)
34 difssd 4131 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βˆ– π‘Œ) βŠ† 𝑋)
35 fri 5635 . . . . . . . . . . . . 13 ((((𝑋 βˆ– π‘Œ) ∈ V ∧ (π‘Šβ€˜π‘‹) Fr 𝑋) ∧ ((𝑋 βˆ– π‘Œ) βŠ† 𝑋 ∧ (𝑋 βˆ– π‘Œ) β‰  βˆ…)) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
3635expr 457 . . . . . . . . . . . 12 ((((𝑋 βˆ– π‘Œ) ∈ V ∧ (π‘Šβ€˜π‘‹) Fr 𝑋) ∧ (𝑋 βˆ– π‘Œ) βŠ† 𝑋) β†’ ((𝑋 βˆ– π‘Œ) β‰  βˆ… β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧))
3729, 33, 34, 36syl21anc 836 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 βˆ– π‘Œ) β‰  βˆ… β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧))
38 ssdif0 4362 . . . . . . . . . . . . . . 15 ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βŠ† π‘Œ ↔ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βˆ– π‘Œ) = βˆ…)
39 indif1 4270 . . . . . . . . . . . . . . . 16 ((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βˆ– π‘Œ)
4039eqeq1i 2737 . . . . . . . . . . . . . . 15 (((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = βˆ… ↔ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βˆ– π‘Œ) = βˆ…)
41 disj 4446 . . . . . . . . . . . . . . . 16 (((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = βˆ… ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
42 vex 3478 . . . . . . . . . . . . . . . . . . . 20 𝑀 ∈ V
4342eliniseg 6090 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V β†’ (𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ 𝑀(π‘Šβ€˜π‘‹)𝑧))
4443elv 3480 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4544notbii 319 . . . . . . . . . . . . . . . . 17 (Β¬ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4645ralbii 3093 . . . . . . . . . . . . . . . 16 (βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4741, 46bitri 274 . . . . . . . . . . . . . . 15 (((𝑋 βˆ– π‘Œ) ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = βˆ… ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
4838, 40, 473bitr2i 298 . . . . . . . . . . . . . 14 ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βŠ† π‘Œ ↔ βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧)
49 cnvimass 6077 . . . . . . . . . . . . . . . . 17 (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† dom (π‘Šβ€˜π‘‹)
5026simprd 496 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋))
51 dmss 5900 . . . . . . . . . . . . . . . . . . 19 ((π‘Šβ€˜π‘‹) βŠ† (𝑋 Γ— 𝑋) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ dom (π‘Šβ€˜π‘‹) βŠ† dom (𝑋 Γ— 𝑋))
53 dmxpid 5927 . . . . . . . . . . . . . . . . . 18 dom (𝑋 Γ— 𝑋) = 𝑋
5452, 53sseqtrdi 4031 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ dom (π‘Šβ€˜π‘‹) βŠ† 𝑋)
5549, 54sstrid 3992 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† 𝑋)
56 sseqin2 4214 . . . . . . . . . . . . . . . 16 ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† 𝑋 ↔ (𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
5755, 56sylib 217 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
5857sseq1d 4012 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 ∩ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})) βŠ† π‘Œ ↔ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ))
5948, 58bitr3id 284 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ))
6059rexbidv 3178 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ))
61 eldifn 4126 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (𝑋 βˆ– π‘Œ) β†’ Β¬ 𝑧 ∈ π‘Œ)
6261ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ Β¬ 𝑧 ∈ π‘Œ)
63 eleq1w 2816 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 = 𝑧 β†’ (𝑀 ∈ π‘Œ ↔ 𝑧 ∈ π‘Œ))
6463notbid 317 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 = 𝑧 β†’ (Β¬ 𝑀 ∈ π‘Œ ↔ Β¬ 𝑧 ∈ π‘Œ))
6562, 64syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑀 = 𝑧 β†’ Β¬ 𝑀 ∈ π‘Œ))
6665con2d 134 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑀 ∈ π‘Œ β†’ Β¬ 𝑀 = 𝑧))
6766imp 407 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ Β¬ 𝑀 = 𝑧)
6862adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ Β¬ 𝑧 ∈ π‘Œ)
69 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))
7069ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))
7170breqd 5158 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 ↔ 𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀))
72 eldifi 4125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝑋 βˆ– π‘Œ) β†’ 𝑧 ∈ 𝑋)
7372ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑧 ∈ 𝑋)
7473adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑧 ∈ 𝑋)
75 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀 ∈ π‘Œ)
76 brxp 5723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 Γ— π‘Œ)𝑀 ↔ (𝑧 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ))
7774, 75, 76sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑧(𝑋 Γ— π‘Œ)𝑀)
78 brin 5199 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀 ↔ (𝑧(π‘Šβ€˜π‘‹)𝑀 ∧ 𝑧(𝑋 Γ— π‘Œ)𝑀))
7978rbaib 539 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 Γ— π‘Œ)𝑀 β†’ (𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑀))
8077, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))𝑀 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑀))
8171, 80bitrd 278 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 ↔ 𝑧(π‘Šβ€˜π‘‹)𝑀))
821, 2fpwwe2lem2 10623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (π‘Œπ‘Šπ‘… ↔ ((π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)) ∧ (𝑅 We π‘Œ ∧ βˆ€π‘¦ ∈ π‘Œ [(◑𝑅 β€œ {𝑦}) / 𝑒](𝑒𝐹(𝑅 ∩ (𝑒 Γ— 𝑒))) = 𝑦))))
8382biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘Œπ‘Šπ‘…) β†’ ((π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)) ∧ (𝑅 We π‘Œ ∧ βˆ€π‘¦ ∈ π‘Œ [(◑𝑅 β€œ {𝑦}) / 𝑒](𝑒𝐹(𝑅 ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
8483adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)) ∧ (𝑅 We π‘Œ ∧ βˆ€π‘¦ ∈ π‘Œ [(◑𝑅 β€œ {𝑦}) / 𝑒](𝑒𝐹(𝑅 ∩ (𝑒 Γ— 𝑒))) = 𝑦)))
8584simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ (π‘Œ βŠ† 𝐴 ∧ 𝑅 βŠ† (π‘Œ Γ— π‘Œ)))
8685simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝑅 βŠ† (π‘Œ Γ— π‘Œ))
8786ad5ant12 754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑅 βŠ† (π‘Œ Γ— π‘Œ))
8887ssbrd 5190 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 β†’ 𝑧(π‘Œ Γ— π‘Œ)𝑀))
89 brxp 5723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(π‘Œ Γ— π‘Œ)𝑀 ↔ (𝑧 ∈ π‘Œ ∧ 𝑀 ∈ π‘Œ))
9089simplbi 498 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧(π‘Œ Γ— π‘Œ)𝑀 β†’ 𝑧 ∈ π‘Œ)
9188, 90syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧𝑅𝑀 β†’ 𝑧 ∈ π‘Œ))
9281, 91sylbird 259 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑧(π‘Šβ€˜π‘‹)𝑀 β†’ 𝑧 ∈ π‘Œ))
9368, 92mtod 197 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀)
9431ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (π‘Šβ€˜π‘‹) We 𝑋)
95 weso 5666 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Šβ€˜π‘‹) We 𝑋 β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (π‘Šβ€˜π‘‹) Or 𝑋)
9713ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘Œ βŠ† 𝑋)
9897sselda 3981 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀 ∈ 𝑋)
99 sotric 5615 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Šβ€˜π‘‹) Or 𝑋 ∧ (𝑀 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ Β¬ (𝑀 = 𝑧 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑀)))
100 ioran 982 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ (𝑀 = 𝑧 ∨ 𝑧(π‘Šβ€˜π‘‹)𝑀) ↔ (Β¬ 𝑀 = 𝑧 ∧ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀))
10199, 100bitrdi 286 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Šβ€˜π‘‹) Or 𝑋 ∧ (𝑀 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ (𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ (Β¬ 𝑀 = 𝑧 ∧ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀)))
10296, 98, 74, 101syl12anc 835 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ (𝑀(π‘Šβ€˜π‘‹)𝑧 ↔ (Β¬ 𝑀 = 𝑧 ∧ Β¬ 𝑧(π‘Šβ€˜π‘‹)𝑀)))
10367, 93, 102mpbir2and 711 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀(π‘Šβ€˜π‘‹)𝑧)
104103, 44sylibr 233 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑀 ∈ π‘Œ) β†’ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
105104ex 413 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑀 ∈ π‘Œ β†’ 𝑀 ∈ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))
106105ssrdv 3987 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘Œ βŠ† (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
107 simprr 771 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)
108106, 107eqssd 3998 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘Œ = (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))
109 in32 4220 . . . . . . . . . . . . . . . . . 18 (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)) ∩ (π‘Œ Γ— π‘Œ)) = (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) ∩ (𝑋 Γ— π‘Œ))
110 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))
111110ineq1d 4210 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑅 ∩ (π‘Œ Γ— π‘Œ)) = (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)) ∩ (π‘Œ Γ— π‘Œ)))
11286ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 βŠ† (π‘Œ Γ— π‘Œ))
113 df-ss 3964 . . . . . . . . . . . . . . . . . . . 20 (𝑅 βŠ† (π‘Œ Γ— π‘Œ) ↔ (𝑅 ∩ (π‘Œ Γ— π‘Œ)) = 𝑅)
114112, 113sylib 217 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (𝑅 ∩ (π‘Œ Γ— π‘Œ)) = 𝑅)
115111, 114eqtr3d 2774 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)) ∩ (π‘Œ Γ— π‘Œ)) = 𝑅)
116 inss2 4228 . . . . . . . . . . . . . . . . . . . 20 ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) βŠ† (π‘Œ Γ— π‘Œ)
117 xpss1 5694 . . . . . . . . . . . . . . . . . . . . 21 (π‘Œ βŠ† 𝑋 β†’ (π‘Œ Γ— π‘Œ) βŠ† (𝑋 Γ— π‘Œ))
11897, 117syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘Œ Γ— π‘Œ) βŠ† (𝑋 Γ— π‘Œ))
119116, 118sstrid 3992 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) βŠ† (𝑋 Γ— π‘Œ))
120 df-ss 3964 . . . . . . . . . . . . . . . . . . 19 (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) βŠ† (𝑋 Γ— π‘Œ) ↔ (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) ∩ (𝑋 Γ— π‘Œ)) = ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)))
121119, 120sylib 217 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) ∩ (𝑋 Γ— π‘Œ)) = ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)))
122109, 115, 1213eqtr3a 2796 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)))
123108sqxpeqd 5707 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘Œ Γ— π‘Œ) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))
124123ineq2d 4211 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ ((π‘Šβ€˜π‘‹) ∩ (π‘Œ Γ— π‘Œ)) = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))))
125122, 124eqtrd 2772 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}))))
126108, 125oveq12d 7423 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘ŒπΉπ‘…) = ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))))
12718adantr 481 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ 𝐴 ∈ 𝑉)
12822adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
129128ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ π‘‹π‘Š(π‘Šβ€˜π‘‹))
1301, 127, 129fpwwe2lem3 10624 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) ∧ 𝑧 ∈ 𝑋) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))) = 𝑧)
13173, 130mpdan 685 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})𝐹((π‘Šβ€˜π‘‹) ∩ ((β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) Γ— (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧})))) = 𝑧)
132126, 131eqtrd 2772 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ (π‘ŒπΉπ‘…) = 𝑧)
133132, 62eqneltrd 2853 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) ∧ (𝑧 ∈ (𝑋 βˆ– π‘Œ) ∧ (β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ)) β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ)
134133rexlimdvaa 3156 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)(β—‘(π‘Šβ€˜π‘‹) β€œ {𝑧}) βŠ† π‘Œ β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ))
13560, 134sylbid 239 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– π‘Œ)βˆ€π‘€ ∈ (𝑋 βˆ– π‘Œ) Β¬ 𝑀(π‘Šβ€˜π‘‹)𝑧 β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ))
13637, 135syld 47 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((𝑋 βˆ– π‘Œ) β‰  βˆ… β†’ Β¬ (π‘ŒπΉπ‘…) ∈ π‘Œ))
137136necon4ad 2959 . . . . . . . . 9 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ ((π‘ŒπΉπ‘…) ∈ π‘Œ β†’ (𝑋 βˆ– π‘Œ) = βˆ…))
13816, 137mpd 15 . . . . . . . 8 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ (𝑋 βˆ– π‘Œ) = βˆ…)
139 ssdif0 4362 . . . . . . . 8 (𝑋 βŠ† π‘Œ ↔ (𝑋 βˆ– π‘Œ) = βˆ…)
140138, 139sylibr 233 . . . . . . 7 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))) β†’ 𝑋 βŠ† π‘Œ)
141140ex 413 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ))) β†’ 𝑋 βŠ† π‘Œ))
1423adantlr 713 . . . . . . 7 (((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) ∧ (π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯)) β†’ (π‘₯πΉπ‘Ÿ) ∈ 𝐴)
143 simprl 769 . . . . . . 7 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œπ‘Šπ‘…)
1441, 17, 142, 128, 143fpwwe2lem9 10630 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ ((𝑋 βŠ† π‘Œ ∧ (π‘Šβ€˜π‘‹) = (𝑅 ∩ (π‘Œ Γ— 𝑋))) ∨ (π‘Œ βŠ† 𝑋 ∧ 𝑅 = ((π‘Šβ€˜π‘‹) ∩ (𝑋 Γ— π‘Œ)))))
14515, 141, 144mpjaod 858 . . . . 5 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝑋 βŠ† π‘Œ)
14613, 145eqssd 3998 . . . 4 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘Œ = 𝑋)
1476adantr 481 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ Fun π‘Š)
148146, 143eqbrtrrd 5171 . . . . . 6 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ π‘‹π‘Šπ‘…)
149 funbrfv 6939 . . . . . 6 (Fun π‘Š β†’ (π‘‹π‘Šπ‘… β†’ (π‘Šβ€˜π‘‹) = 𝑅))
150147, 148, 149sylc 65 . . . . 5 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ (π‘Šβ€˜π‘‹) = 𝑅)
151150eqcomd 2738 . . . 4 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ 𝑅 = (π‘Šβ€˜π‘‹))
152146, 151jca 512 . . 3 ((πœ‘ ∧ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)) β†’ (π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)))
153152ex 413 . 2 (πœ‘ β†’ ((π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ) β†’ (π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹))))
1541, 2, 3, 4fpwwe2lem12 10633 . . . 4 (πœ‘ β†’ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)
15522, 154jca 512 . . 3 (πœ‘ β†’ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
156 breq12 5152 . . . 4 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ (π‘Œπ‘Šπ‘… ↔ π‘‹π‘Š(π‘Šβ€˜π‘‹)))
157 oveq12 7414 . . . . 5 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ (π‘ŒπΉπ‘…) = (𝑋𝐹(π‘Šβ€˜π‘‹)))
158 simpl 483 . . . . 5 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ π‘Œ = 𝑋)
159157, 158eleq12d 2827 . . . 4 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ ((π‘ŒπΉπ‘…) ∈ π‘Œ ↔ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋))
160156, 159anbi12d 631 . . 3 ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ ((π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ) ↔ (π‘‹π‘Š(π‘Šβ€˜π‘‹) ∧ (𝑋𝐹(π‘Šβ€˜π‘‹)) ∈ 𝑋)))
161155, 160syl5ibrcom 246 . 2 (πœ‘ β†’ ((π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹)) β†’ (π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ)))
162153, 161impbid 211 1 (πœ‘ β†’ ((π‘Œπ‘Šπ‘… ∧ (π‘ŒπΉπ‘…) ∈ π‘Œ) ↔ (π‘Œ = 𝑋 ∧ 𝑅 = (π‘Šβ€˜π‘‹))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474  [wsbc 3776   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907   class class class wbr 5147  {copab 5209   Or wor 5586   Fr wfr 5627   We wwe 5629   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675   β€œ cima 5678  Fun wfun 6534  β€˜cfv 6540  (class class class)co 7405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-oi 9501
This theorem is referenced by:  fpwwe  10637  canthwelem  10641  pwfseqlem4  10653
  Copyright terms: Public domain W3C validator