MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssenen Structured version   Visualization version   GIF version
Theorem ssenen 9150
Description: Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
Assertion
Ref Expression
ssenen (𝐴 β‰ˆ 𝐡 β†’ {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)} β‰ˆ {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)})
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐡   π‘₯,𝐢
Proof of Theorem ssenen
Dummy variables 𝑦 𝑧 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 8948 . . 3 (𝐴 β‰ˆ 𝐡 ↔ βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡)
2 f1odm 6830 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ dom 𝑓 = 𝐴)
3 vex 3472 . . . . . . . 8 𝑓 ∈ V
43dmex 7898 . . . . . . 7 dom 𝑓 ∈ V
52, 4eqeltrrdi 2836 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐴 ∈ V)
6 pwexg 5369 . . . . . 6 (𝐴 ∈ V β†’ 𝒫 𝐴 ∈ V)
7 inex1g 5312 . . . . . 6 (𝒫 𝐴 ∈ V β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
85, 6, 73syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
9 f1ofo 6833 . . . . . . . 8 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–onto→𝐡)
10 forn 6801 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ ran 𝑓 = 𝐡)
119, 10syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ran 𝑓 = 𝐡)
123rnex 7899 . . . . . . 7 ran 𝑓 ∈ V
1311, 12eqeltrrdi 2836 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐡 ∈ V)
14 pwexg 5369 . . . . . 6 (𝐡 ∈ V β†’ 𝒫 𝐡 ∈ V)
15 inex1g 5312 . . . . . 6 (𝒫 𝐡 ∈ V β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
1613, 14, 153syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
17 f1of1 6825 . . . . . . . . . . 11 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–1-1→𝐡)
1817adantr 480 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑓:𝐴–1-1→𝐡)
1913adantr 480 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝐡 ∈ V)
20 simpr 484 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 βŠ† 𝐴)
21 vex 3472 . . . . . . . . . . 11 𝑦 ∈ V
2221a1i 11 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 ∈ V)
23 f1imaen2g 9010 . . . . . . . . . 10 (((𝑓:𝐴–1-1→𝐡 ∧ 𝐡 ∈ V) ∧ (𝑦 βŠ† 𝐴 ∧ 𝑦 ∈ V)) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
2418, 19, 20, 22, 23syl22anc 836 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
25 entr 9001 . . . . . . . . 9 (((𝑓 β€œ 𝑦) β‰ˆ 𝑦 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2624, 25sylan 579 . . . . . . . 8 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2726expl 457 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
28 imassrn 6063 . . . . . . . . 9 (𝑓 β€œ 𝑦) βŠ† ran 𝑓
2928, 10sseqtrid 4029 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
309, 29syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
3127, 30jctild 525 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)))
32 elin 3959 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
3321elpw 4601 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 βŠ† 𝐴)
34 breq1 5144 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑦 β‰ˆ 𝐢))
3521, 34elab 3663 . . . . . . . 8 (𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑦 β‰ˆ 𝐢)
3633, 35anbi12i 626 . . . . . . 7 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
3732, 36bitri 275 . . . . . 6 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
38 elin 3959 . . . . . . 7 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
393imaex 7903 . . . . . . . . 9 (𝑓 β€œ 𝑦) ∈ V
4039elpw 4601 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ↔ (𝑓 β€œ 𝑦) βŠ† 𝐡)
41 breq1 5144 . . . . . . . . 9 (π‘₯ = (𝑓 β€œ 𝑦) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4239, 41elab 3663 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
4340, 42anbi12i 626 . . . . . . 7 (((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4438, 43bitri 275 . . . . . 6 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4531, 37, 443imtr4g 296 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
46 f1ocnv 6838 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1-onto→𝐴)
47 f1of1 6825 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1→𝐴)
48 f1f1orn 6837 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1→𝐴 β†’ ◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓)
49 f1of1 6825 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
5047, 48, 493syl 18 . . . . . . . . . . 11 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
51 vex 3472 . . . . . . . . . . . 12 𝑧 ∈ V
5251f1imaen 9011 . . . . . . . . . . 11 ((◑𝑓:𝐡–1-1β†’ran ◑𝑓 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
5350, 52sylan 579 . . . . . . . . . 10 ((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
54 entr 9001 . . . . . . . . . 10 (((◑𝑓 β€œ 𝑧) β‰ˆ 𝑧 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5553, 54sylan 579 . . . . . . . . 9 (((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5655expl 457 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
57 f1ofo 6833 . . . . . . . . 9 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–onto→𝐴)
58 imassrn 6063 . . . . . . . . . 10 (◑𝑓 β€œ 𝑧) βŠ† ran ◑𝑓
59 forn 6801 . . . . . . . . . 10 (◑𝑓:𝐡–onto→𝐴 β†’ ran ◑𝑓 = 𝐴)
6058, 59sseqtrid 4029 . . . . . . . . 9 (◑𝑓:𝐡–onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6157, 60syl 17 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6256, 61jctild 525 . . . . . . 7 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
6346, 62syl 17 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
64 elin 3959 . . . . . . 7 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
6551elpw 4601 . . . . . . . 8 (𝑧 ∈ 𝒫 𝐡 ↔ 𝑧 βŠ† 𝐡)
66 breq1 5144 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑧 β‰ˆ 𝐢))
6751, 66elab 3663 . . . . . . . 8 (𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑧 β‰ˆ 𝐢)
6865, 67anbi12i 626 . . . . . . 7 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
6964, 68bitri 275 . . . . . 6 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
70 elin 3959 . . . . . . 7 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
713cnvex 7912 . . . . . . . . . 10 ◑𝑓 ∈ V
7271imaex 7903 . . . . . . . . 9 (◑𝑓 β€œ 𝑧) ∈ V
7372elpw 4601 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ↔ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
74 breq1 5144 . . . . . . . . 9 (π‘₯ = (◑𝑓 β€œ 𝑧) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7572, 74elab 3663 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
7673, 75anbi12i 626 . . . . . . 7 (((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7770, 76bitri 275 . . . . . 6 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7863, 69, 773imtr4g 296 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
79 simpl 482 . . . . . . . . . . 11 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 ∈ 𝒫 𝐡)
8079elpwid 4606 . . . . . . . . . 10 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
8164, 80sylbi 216 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
82 imaeq2 6048 . . . . . . . . . . . 12 (𝑦 = (◑𝑓 β€œ 𝑧) β†’ (𝑓 β€œ 𝑦) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
83 f1orel 6829 . . . . . . . . . . . . . . . 16 (𝑓:𝐴–1-1-onto→𝐡 β†’ Rel 𝑓)
84 dfrel2 6181 . . . . . . . . . . . . . . . 16 (Rel 𝑓 ↔ ◑◑𝑓 = 𝑓)
8583, 84sylib 217 . . . . . . . . . . . . . . 15 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑◑𝑓 = 𝑓)
8685imaeq1d 6051 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8786adantr 480 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8846, 47syl 17 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1→𝐴)
89 f1imacnv 6842 . . . . . . . . . . . . . 14 ((◑𝑓:𝐡–1-1→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9088, 89sylan 579 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9187, 90eqtr3d 2768 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9282, 91sylan9eqr 2788 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ (𝑓 β€œ 𝑦) = 𝑧)
9392eqcomd 2732 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ 𝑧 = (𝑓 β€œ 𝑦))
9493ex 412 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9581, 94sylan2 592 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9695adantrl 713 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
97 simpl 482 . . . . . . . . . . 11 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 ∈ 𝒫 𝐴)
9897elpwid 4606 . . . . . . . . . 10 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
9932, 98sylbi 216 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
100 imaeq2 6048 . . . . . . . . . . . 12 (𝑧 = (𝑓 β€œ 𝑦) β†’ (◑𝑓 β€œ 𝑧) = (◑𝑓 β€œ (𝑓 β€œ 𝑦)))
101 f1imacnv 6842 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
10217, 101sylan 579 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
103100, 102sylan9eqr 2788 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ (◑𝑓 β€œ 𝑧) = 𝑦)
104103eqcomd 2732 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ 𝑦 = (◑𝑓 β€œ 𝑧))
105104ex 412 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10699, 105sylan2 592 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
107106adantrr 714 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10896, 107impbid 211 . . . . . 6 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦)))
109108ex 412 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦))))
1108, 16, 45, 78, 109en3d 8984 . . . 4 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
111110exlimiv 1925 . . 3 (βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
1121, 111sylbi 216 . 2 (𝐴 β‰ˆ 𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
113 df-pw 4599 . . . 4 𝒫 𝐴 = {π‘₯ ∣ π‘₯ βŠ† 𝐴}
114113ineq1i 4203 . . 3 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
115 inab 4294 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
116114, 115eqtri 2754 . 2 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
117 df-pw 4599 . . . 4 𝒫 𝐡 = {π‘₯ ∣ π‘₯ βŠ† 𝐡}
118117ineq1i 4203 . . 3 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
119 inab 4294 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
120118, 119eqtri 2754 . 2 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
121112, 116, 1203brtr3g 5174 1 (𝐴 β‰ˆ 𝐡 β†’ {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)} β‰ˆ {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  {cab 2703  Vcvv 3468   ∩ cin 3942   βŠ† wss 3943  π’« cpw 4597   class class class wbr 5141  β—‘ccnv 5668  dom cdm 5669  ran crn 5670   β€œ cima 5672  Rel wrel 5674  β€“1-1β†’wf1 6533  β€“ontoβ†’wfo 6534  β€“1-1-ontoβ†’wf1o 6535   β‰ˆ cen 8935
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 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8702  df-en 8939
This theorem is referenced by:  infmap2  10212
  Copyright terms: Public domain W3C validator