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 32139
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 6075 . . . 4 (2nd ā€œ āˆ…) = āˆ…
2 xpeq2 5696 . . . . . 6 (šµ = āˆ… → (š“ Ɨ šµ) = (š“ Ɨ āˆ…))
3 xp0 6156 . . . . . 6 (š“ Ɨ āˆ…) = āˆ…
42, 3eqtrdi 2786 . . . . 5 (šµ = āˆ… → (š“ Ɨ šµ) = āˆ…)
54imaeq2d 6058 . . . 4 (šµ = āˆ… → (2nd ā€œ (š“ Ɨ šµ)) = (2nd ā€œ āˆ…))
6 id 22 . . . 4 (šµ = āˆ… → šµ = āˆ…)
71, 5, 63eqtr4a 2796 . . 3 (šµ = āˆ… → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
87adantl 480 . 2 ((š“ ≠ āˆ… ∧ šµ = āˆ…) → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
9 xpnz 6157 . . . . 5 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ↔ (š“ Ɨ šµ) ≠ āˆ…)
10 fo2nd 7998 . . . . . . 7 2nd :V–onto→V
11 fofn 6806 . . . . . . 7 (2nd :V–onto→V → 2nd Fn V)
1210, 11mp1i 13 . . . . . 6 ((š“ Ɨ šµ) ≠ āˆ… → 2nd Fn V)
13 ssv 4005 . . . . . . 7 (š“ Ɨ šµ) āŠ† V
1413a1i 11 . . . . . 6 ((š“ Ɨ šµ) ≠ āˆ… → (š“ Ɨ šµ) āŠ† V)
1512, 14fvelimabd 6964 . . . . 5 ((š“ Ɨ šµ) ≠ āˆ… → (š‘¦ ∈ (2nd ā€œ (š“ Ɨ šµ)) ↔ āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦))
169, 15sylbi 216 . . . 4 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (š‘¦ ∈ (2nd ā€œ (š“ Ɨ šµ)) ↔ āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦))
17 simpr 483 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘ ∈ (š“ Ɨ šµ)) ∧ (2nd ā€˜š‘) = š‘¦) → (2nd ā€˜š‘) = š‘¦)
18 xp2nd 8010 . . . . . . . 8 (š‘ ∈ (š“ Ɨ šµ) → (2nd ā€˜š‘) ∈ šµ)
1918ad2antlr 723 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘ ∈ (š“ Ɨ šµ)) ∧ (2nd ā€˜š‘) = š‘¦) → (2nd ā€˜š‘) ∈ šµ)
2017, 19eqeltrrd 2832 . . . . . 6 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘ ∈ (š“ Ɨ šµ)) ∧ (2nd ā€˜š‘) = š‘¦) → š‘¦ ∈ šµ)
2120r19.29an 3156 . . . . 5 (((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦) → š‘¦ ∈ šµ)
22 n0 4345 . . . . . . . 8 (š“ ≠ āˆ… ↔ āˆƒš‘„ š‘„ ∈ š“)
2322biimpi 215 . . . . . . 7 (š“ ≠ āˆ… → āˆƒš‘„ š‘„ ∈ š“)
2423ad2antrr 722 . . . . . 6 (((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) → āˆƒš‘„ š‘„ ∈ š“)
25 opelxpi 5712 . . . . . . . . 9 ((š‘„ ∈ š“ ∧ š‘¦ ∈ šµ) → āŸØš‘„, š‘¦āŸ© ∈ (š“ Ɨ šµ))
2625ancoms 457 . . . . . . . 8 ((š‘¦ ∈ šµ ∧ š‘„ ∈ š“) → āŸØš‘„, š‘¦āŸ© ∈ (š“ Ɨ šµ))
2726adantll 710 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) → āŸØš‘„, š‘¦āŸ© ∈ (š“ Ɨ šµ))
28 fveqeq2 6899 . . . . . . . 8 (š‘ = āŸØš‘„, š‘¦āŸ© → ((2nd ā€˜š‘) = š‘¦ ↔ (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦))
2928adantl 480 . . . . . . 7 (((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) ∧ š‘ = āŸØš‘„, š‘¦āŸ©) → ((2nd ā€˜š‘) = š‘¦ ↔ (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦))
30 vex 3476 . . . . . . . . 9 š‘„ ∈ V
31 vex 3476 . . . . . . . . 9 š‘¦ ∈ V
3230, 31op2nd 7986 . . . . . . . 8 (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦
3332a1i 11 . . . . . . 7 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) → (2nd ā€˜āŸØš‘„, š‘¦āŸ©) = š‘¦)
3427, 29, 33rspcedvd 3613 . . . . . 6 ((((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) ∧ š‘„ ∈ š“) → āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦)
3524, 34exlimddv 1936 . . . . 5 (((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) ∧ š‘¦ ∈ šµ) → āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦)
3621, 35impbida 797 . . . 4 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (āˆƒš‘ ∈ (š“ Ɨ šµ)(2nd ā€˜š‘) = š‘¦ ↔ š‘¦ ∈ šµ))
3716, 36bitrd 278 . . 3 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (š‘¦ ∈ (2nd ā€œ (š“ Ɨ šµ)) ↔ š‘¦ ∈ šµ))
3837eqrdv 2728 . 2 ((š“ ≠ āˆ… ∧ šµ ≠ āˆ…) → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
398, 38pm2.61dane 3027 1 (š“ ≠ āˆ… → (2nd ā€œ (š“ Ɨ šµ)) = šµ)
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539  āˆƒwex 1779   ∈ wcel 2104   ≠ wne 2938  āˆƒwrex 3068  Vcvv 3472   āŠ† wss 3947  āˆ…c0 4321  āŸØcop 4633   Ɨ cxp 5673   ā€œ cima 5678   Fn wfn 6537  ā€“onto→wfo 6540  ā€˜cfv 6542  2nd c2nd 7976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  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-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fo 6548  df-fv 6550  df-2nd 7978
This theorem is referenced by:  gsumpart  32477
  Copyright terms: Public domain W3C validator