MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssenen Structured version   Visualization version   GIF version
Theorem ssenen 9147
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 8945 . . 3 (𝐴 β‰ˆ 𝐡 ↔ βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡)
2 f1odm 6834 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ dom 𝑓 = 𝐴)
3 vex 3478 . . . . . . . 8 𝑓 ∈ V
43dmex 7898 . . . . . . 7 dom 𝑓 ∈ V
52, 4eqeltrrdi 2842 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐴 ∈ V)
6 pwexg 5375 . . . . . 6 (𝐴 ∈ V β†’ 𝒫 𝐴 ∈ V)
7 inex1g 5318 . . . . . 6 (𝒫 𝐴 ∈ V β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
85, 6, 73syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
9 f1ofo 6837 . . . . . . . 8 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–onto→𝐡)
10 forn 6805 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ ran 𝑓 = 𝐡)
119, 10syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ran 𝑓 = 𝐡)
123rnex 7899 . . . . . . 7 ran 𝑓 ∈ V
1311, 12eqeltrrdi 2842 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐡 ∈ V)
14 pwexg 5375 . . . . . 6 (𝐡 ∈ V β†’ 𝒫 𝐡 ∈ V)
15 inex1g 5318 . . . . . 6 (𝒫 𝐡 ∈ V β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
1613, 14, 153syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
17 f1of1 6829 . . . . . . . . . . 11 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–1-1→𝐡)
1817adantr 481 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑓:𝐴–1-1→𝐡)
1913adantr 481 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝐡 ∈ V)
20 simpr 485 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 βŠ† 𝐴)
21 vex 3478 . . . . . . . . . . 11 𝑦 ∈ V
2221a1i 11 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 ∈ V)
23 f1imaen2g 9007 . . . . . . . . . 10 (((𝑓:𝐴–1-1→𝐡 ∧ 𝐡 ∈ V) ∧ (𝑦 βŠ† 𝐴 ∧ 𝑦 ∈ V)) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
2418, 19, 20, 22, 23syl22anc 837 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
25 entr 8998 . . . . . . . . 9 (((𝑓 β€œ 𝑦) β‰ˆ 𝑦 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2624, 25sylan 580 . . . . . . . 8 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2726expl 458 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
28 imassrn 6068 . . . . . . . . 9 (𝑓 β€œ 𝑦) βŠ† ran 𝑓
2928, 10sseqtrid 4033 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
309, 29syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
3127, 30jctild 526 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)))
32 elin 3963 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
3321elpw 4605 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 βŠ† 𝐴)
34 breq1 5150 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑦 β‰ˆ 𝐢))
3521, 34elab 3667 . . . . . . . 8 (𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑦 β‰ˆ 𝐢)
3633, 35anbi12i 627 . . . . . . 7 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
3732, 36bitri 274 . . . . . 6 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
38 elin 3963 . . . . . . 7 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
393imaex 7903 . . . . . . . . 9 (𝑓 β€œ 𝑦) ∈ V
4039elpw 4605 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ↔ (𝑓 β€œ 𝑦) βŠ† 𝐡)
41 breq1 5150 . . . . . . . . 9 (π‘₯ = (𝑓 β€œ 𝑦) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4239, 41elab 3667 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
4340, 42anbi12i 627 . . . . . . 7 (((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4438, 43bitri 274 . . . . . 6 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4531, 37, 443imtr4g 295 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
46 f1ocnv 6842 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1-onto→𝐴)
47 f1of1 6829 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1→𝐴)
48 f1f1orn 6841 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1→𝐴 β†’ ◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓)
49 f1of1 6829 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
5047, 48, 493syl 18 . . . . . . . . . . 11 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
51 vex 3478 . . . . . . . . . . . 12 𝑧 ∈ V
5251f1imaen 9008 . . . . . . . . . . 11 ((◑𝑓:𝐡–1-1β†’ran ◑𝑓 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
5350, 52sylan 580 . . . . . . . . . 10 ((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
54 entr 8998 . . . . . . . . . 10 (((◑𝑓 β€œ 𝑧) β‰ˆ 𝑧 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5553, 54sylan 580 . . . . . . . . 9 (((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5655expl 458 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
57 f1ofo 6837 . . . . . . . . 9 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–onto→𝐴)
58 imassrn 6068 . . . . . . . . . 10 (◑𝑓 β€œ 𝑧) βŠ† ran ◑𝑓
59 forn 6805 . . . . . . . . . 10 (◑𝑓:𝐡–onto→𝐴 β†’ ran ◑𝑓 = 𝐴)
6058, 59sseqtrid 4033 . . . . . . . . 9 (◑𝑓:𝐡–onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6157, 60syl 17 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6256, 61jctild 526 . . . . . . 7 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
6346, 62syl 17 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
64 elin 3963 . . . . . . 7 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
6551elpw 4605 . . . . . . . 8 (𝑧 ∈ 𝒫 𝐡 ↔ 𝑧 βŠ† 𝐡)
66 breq1 5150 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑧 β‰ˆ 𝐢))
6751, 66elab 3667 . . . . . . . 8 (𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑧 β‰ˆ 𝐢)
6865, 67anbi12i 627 . . . . . . 7 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
6964, 68bitri 274 . . . . . 6 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
70 elin 3963 . . . . . . 7 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
713cnvex 7912 . . . . . . . . . 10 ◑𝑓 ∈ V
7271imaex 7903 . . . . . . . . 9 (◑𝑓 β€œ 𝑧) ∈ V
7372elpw 4605 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ↔ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
74 breq1 5150 . . . . . . . . 9 (π‘₯ = (◑𝑓 β€œ 𝑧) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7572, 74elab 3667 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
7673, 75anbi12i 627 . . . . . . 7 (((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7770, 76bitri 274 . . . . . 6 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7863, 69, 773imtr4g 295 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
79 simpl 483 . . . . . . . . . . 11 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 ∈ 𝒫 𝐡)
8079elpwid 4610 . . . . . . . . . 10 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
8164, 80sylbi 216 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
82 imaeq2 6053 . . . . . . . . . . . 12 (𝑦 = (◑𝑓 β€œ 𝑧) β†’ (𝑓 β€œ 𝑦) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
83 f1orel 6833 . . . . . . . . . . . . . . . 16 (𝑓:𝐴–1-1-onto→𝐡 β†’ Rel 𝑓)
84 dfrel2 6185 . . . . . . . . . . . . . . . 16 (Rel 𝑓 ↔ ◑◑𝑓 = 𝑓)
8583, 84sylib 217 . . . . . . . . . . . . . . 15 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑◑𝑓 = 𝑓)
8685imaeq1d 6056 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8786adantr 481 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8846, 47syl 17 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1→𝐴)
89 f1imacnv 6846 . . . . . . . . . . . . . 14 ((◑𝑓:𝐡–1-1→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9088, 89sylan 580 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9187, 90eqtr3d 2774 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9282, 91sylan9eqr 2794 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ (𝑓 β€œ 𝑦) = 𝑧)
9392eqcomd 2738 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ 𝑧 = (𝑓 β€œ 𝑦))
9493ex 413 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9581, 94sylan2 593 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9695adantrl 714 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
97 simpl 483 . . . . . . . . . . 11 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 ∈ 𝒫 𝐴)
9897elpwid 4610 . . . . . . . . . 10 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
9932, 98sylbi 216 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
100 imaeq2 6053 . . . . . . . . . . . 12 (𝑧 = (𝑓 β€œ 𝑦) β†’ (◑𝑓 β€œ 𝑧) = (◑𝑓 β€œ (𝑓 β€œ 𝑦)))
101 f1imacnv 6846 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
10217, 101sylan 580 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
103100, 102sylan9eqr 2794 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ (◑𝑓 β€œ 𝑧) = 𝑦)
104103eqcomd 2738 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ 𝑦 = (◑𝑓 β€œ 𝑧))
105104ex 413 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10699, 105sylan2 593 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
107106adantrr 715 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10896, 107impbid 211 . . . . . 6 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦)))
109108ex 413 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦))))
1108, 16, 45, 78, 109en3d 8981 . . . 4 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
111110exlimiv 1933 . . 3 (βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
1121, 111sylbi 216 . 2 (𝐴 β‰ˆ 𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
113 df-pw 4603 . . . 4 𝒫 𝐴 = {π‘₯ ∣ π‘₯ βŠ† 𝐴}
114113ineq1i 4207 . . 3 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
115 inab 4298 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
116114, 115eqtri 2760 . 2 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
117 df-pw 4603 . . . 4 𝒫 𝐡 = {π‘₯ ∣ π‘₯ βŠ† 𝐡}
118117ineq1i 4207 . . 3 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
119 inab 4298 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
120118, 119eqtri 2760 . 2 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
121112, 116, 1203brtr3g 5180 1 (𝐴 β‰ˆ 𝐡 β†’ {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)} β‰ˆ {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2709  Vcvv 3474   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601   class class class wbr 5147  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678  Rel wrel 5680  β€“1-1β†’wf1 6537  β€“ontoβ†’wfo 6538  β€“1-1-ontoβ†’wf1o 6539   β‰ˆ cen 8932
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-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-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-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  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 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8699  df-en 8936
This theorem is referenced by:  infmap2  10209
  Copyright terms: Public domain W3C validator