Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2ndimaxp Structured version   Visualization version   GIF version

Theorem 2ndimaxp 32140
Description: Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.)
Assertion
Ref Expression
2ndimaxp (š“ ≠ āˆ… → (2nd ā€œ (š“ Ɨ šµ)) = šµ)

Proof of Theorem 2ndimaxp
Dummy variables š‘ š‘„ š‘¦ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ima0 6076 . . . 4 (2nd ā€œ āˆ…) = āˆ…
2 xpeq2 5697 . . . . . 6 (šµ = āˆ… → (š“ Ɨ šµ) = (š“ Ɨ āˆ…))
3 xp0 6157 . . . . . 6 (š“ Ɨ āˆ…) = āˆ…
42, 3eqtrdi 2787 . . . . 5 (šµ = āˆ… → (š“ Ɨ šµ) = āˆ…)
54imaeq2d 6059 . . . 4 (šµ = āˆ… → (2nd ā€œ (š“ Ɨ šµ)) = (2nd ā€œ āˆ…))
6 id 22 . . . 4 (šµ = āˆ… → šµ = āˆ…)
71, 5, 63eqtr4a 2797 . . 3 (šµ = āˆ… → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
87adantl 481 . 2 ((š“ ≠ āˆ… ∧ šµ = āˆ…) → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
9 xpnz 6158 . . . . 5 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ↔ (š“ Ɨ šµ) ≠ āˆ…)
10 fo2nd 7999 . . . . . . 7 2nd :V–onto→V
11 fofn 6807 . . . . . . 7 (2nd :V–onto→V → 2nd Fn V)
1210, 11mp1i 13 . . . . . 6 ((š“ Ɨ šµ) ≠ āˆ… → 2nd Fn V)
13 ssv 4006 . . . . . . 7 (š“ Ɨ šµ) āŠ† V
1413a1i 11 . . . . . 6 ((š“ Ɨ šµ) ≠ āˆ… → (š“ Ɨ šµ) āŠ† V)
1512, 14fvelimabd 6965 . . . . 5 ((š“ Ɨ šµ) ≠ āˆ… → (š‘¦ ∈ (2nd ā€œ (š“ Ɨ šµ)) ↔ āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦))
169, 15sylbi 216 . . . 4 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (š‘¦ ∈ (2nd ā€œ (š“ Ɨ šµ)) ↔ āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦))
17 simpr 484 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘ ∈ (š“ Ɨ šµ)) ∧ (2nd ā€˜š‘) = š‘¦) → (2nd ā€˜š‘) = š‘¦)
18 xp2nd 8011 . . . . . . . 8 (š‘ ∈ (š“ Ɨ šµ) → (2nd ā€˜š‘) ∈ šµ)
1918ad2antlr 724 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘ ∈ (š“ Ɨ šµ)) ∧ (2nd ā€˜š‘) = š‘¦) → (2nd ā€˜š‘) ∈ šµ)
2017, 19eqeltrrd 2833 . . . . . 6 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘ ∈ (š“ Ɨ šµ)) ∧ (2nd ā€˜š‘) = š‘¦) → š‘¦ ∈ šµ)
2120r19.29an 3157 . . . . 5 (((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦) → š‘¦ ∈ šµ)
22 n0 4346 . . . . . . . 8 (š“ ≠ āˆ… ↔ āˆƒš‘„ š‘„ ∈ š“)
2322biimpi 215 . . . . . . 7 (š“ ≠ āˆ… → āˆƒš‘„ š‘„ ∈ š“)
2423ad2antrr 723 . . . . . 6 (((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) → āˆƒš‘„ š‘„ ∈ š“)
25 opelxpi 5713 . . . . . . . . 9 ((š‘„ ∈ š“ ∧ š‘¦ ∈ šµ) → āŸØš‘„, š‘¦āŸ© ∈ (š“ Ɨ šµ))
2625ancoms 458 . . . . . . . 8 ((š‘¦ ∈ šµ ∧ š‘„ ∈ š“) → āŸØš‘„, š‘¦āŸ© ∈ (š“ Ɨ šµ))
2726adantll 711 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) → āŸØš‘„, š‘¦āŸ© ∈ (š“ Ɨ šµ))
28 fveqeq2 6900 . . . . . . . 8 (š‘ = āŸØš‘„, š‘¦āŸ© → ((2nd ā€˜š‘) = š‘¦ ↔ (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦))
2928adantl 481 . . . . . . 7 (((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) ∧ š‘ = āŸØš‘„, š‘¦āŸ©) → ((2nd ā€˜š‘) = š‘¦ ↔ (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦))
30 vex 3477 . . . . . . . . 9 š‘„ ∈ V
31 vex 3477 . . . . . . . . 9 š‘¦ ∈ V
3230, 31op2nd 7987 . . . . . . . 8 (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦
3332a1i 11 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) → (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦)
3427, 29, 33rspcedvd 3614 . . . . . 6 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) → āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦)
3524, 34exlimddv 1937 . . . . 5 (((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) → āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦)
3621, 35impbida 798 . . . 4 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦ ↔ š‘¦ ∈ šµ))
3716, 36bitrd 279 . . 3 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (š‘¦ ∈ (2nd ā€œ (š“ Ɨ šµ)) ↔ š‘¦ ∈ šµ))
3837eqrdv 2729 . 2 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
398, 38pm2.61dane 3028 1 (š“ ≠ āˆ… → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540  āˆƒwex 1780   ∈ wcel 2105   ≠ wne 2939  āˆƒwrex 3069  Vcvv 3473   āŠ† wss 3948  āˆ…c0 4322  āŸØcop 4634   Ɨ cxp 5674   ā€œ cima 5679   Fn wfn 6538  ā€“onto→wfo 6541  ā€˜cfv 6543  2nd c2nd 7977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fo 6549  df-fv 6551  df-2nd 7979
This theorem is referenced by:  gsumpart  32478
  Copyright terms: Public domain W3C validator