MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssenen Structured version   Visualization version   GIF version

Theorem ssenen 9098
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 8896 . . 3 (𝐴 β‰ˆ 𝐡 ↔ βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡)
2 f1odm 6789 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ dom 𝑓 = 𝐴)
3 vex 3448 . . . . . . . 8 𝑓 ∈ V
43dmex 7849 . . . . . . 7 dom 𝑓 ∈ V
52, 4eqeltrrdi 2843 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐴 ∈ V)
6 pwexg 5334 . . . . . 6 (𝐴 ∈ V β†’ 𝒫 𝐴 ∈ V)
7 inex1g 5277 . . . . . 6 (𝒫 𝐴 ∈ V β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
85, 6, 73syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
9 f1ofo 6792 . . . . . . . 8 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–onto→𝐡)
10 forn 6760 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ ran 𝑓 = 𝐡)
119, 10syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ran 𝑓 = 𝐡)
123rnex 7850 . . . . . . 7 ran 𝑓 ∈ V
1311, 12eqeltrrdi 2843 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐡 ∈ V)
14 pwexg 5334 . . . . . 6 (𝐡 ∈ V β†’ 𝒫 𝐡 ∈ V)
15 inex1g 5277 . . . . . 6 (𝒫 𝐡 ∈ V β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
1613, 14, 153syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
17 f1of1 6784 . . . . . . . . . . 11 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–1-1→𝐡)
1817adantr 482 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑓:𝐴–1-1→𝐡)
1913adantr 482 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝐡 ∈ V)
20 simpr 486 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 βŠ† 𝐴)
21 vex 3448 . . . . . . . . . . 11 𝑦 ∈ V
2221a1i 11 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 ∈ V)
23 f1imaen2g 8958 . . . . . . . . . 10 (((𝑓:𝐴–1-1→𝐡 ∧ 𝐡 ∈ V) ∧ (𝑦 βŠ† 𝐴 ∧ 𝑦 ∈ V)) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
2418, 19, 20, 22, 23syl22anc 838 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
25 entr 8949 . . . . . . . . 9 (((𝑓 β€œ 𝑦) β‰ˆ 𝑦 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2624, 25sylan 581 . . . . . . . 8 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2726expl 459 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
28 imassrn 6025 . . . . . . . . 9 (𝑓 β€œ 𝑦) βŠ† ran 𝑓
2928, 10sseqtrid 3997 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
309, 29syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
3127, 30jctild 527 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)))
32 elin 3927 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
3321elpw 4565 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 βŠ† 𝐴)
34 breq1 5109 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑦 β‰ˆ 𝐢))
3521, 34elab 3631 . . . . . . . 8 (𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑦 β‰ˆ 𝐢)
3633, 35anbi12i 628 . . . . . . 7 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
3732, 36bitri 275 . . . . . 6 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
38 elin 3927 . . . . . . 7 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
393imaex 7854 . . . . . . . . 9 (𝑓 β€œ 𝑦) ∈ V
4039elpw 4565 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ↔ (𝑓 β€œ 𝑦) βŠ† 𝐡)
41 breq1 5109 . . . . . . . . 9 (π‘₯ = (𝑓 β€œ 𝑦) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4239, 41elab 3631 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
4340, 42anbi12i 628 . . . . . . 7 (((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4438, 43bitri 275 . . . . . 6 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4531, 37, 443imtr4g 296 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
46 f1ocnv 6797 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1-onto→𝐴)
47 f1of1 6784 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1→𝐴)
48 f1f1orn 6796 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1→𝐴 β†’ ◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓)
49 f1of1 6784 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
5047, 48, 493syl 18 . . . . . . . . . . 11 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
51 vex 3448 . . . . . . . . . . . 12 𝑧 ∈ V
5251f1imaen 8959 . . . . . . . . . . 11 ((◑𝑓:𝐡–1-1β†’ran ◑𝑓 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
5350, 52sylan 581 . . . . . . . . . 10 ((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
54 entr 8949 . . . . . . . . . 10 (((◑𝑓 β€œ 𝑧) β‰ˆ 𝑧 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5553, 54sylan 581 . . . . . . . . 9 (((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5655expl 459 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
57 f1ofo 6792 . . . . . . . . 9 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–onto→𝐴)
58 imassrn 6025 . . . . . . . . . 10 (◑𝑓 β€œ 𝑧) βŠ† ran ◑𝑓
59 forn 6760 . . . . . . . . . 10 (◑𝑓:𝐡–onto→𝐴 β†’ ran ◑𝑓 = 𝐴)
6058, 59sseqtrid 3997 . . . . . . . . 9 (◑𝑓:𝐡–onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6157, 60syl 17 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6256, 61jctild 527 . . . . . . 7 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
6346, 62syl 17 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
64 elin 3927 . . . . . . 7 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
6551elpw 4565 . . . . . . . 8 (𝑧 ∈ 𝒫 𝐡 ↔ 𝑧 βŠ† 𝐡)
66 breq1 5109 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑧 β‰ˆ 𝐢))
6751, 66elab 3631 . . . . . . . 8 (𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑧 β‰ˆ 𝐢)
6865, 67anbi12i 628 . . . . . . 7 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
6964, 68bitri 275 . . . . . 6 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
70 elin 3927 . . . . . . 7 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
713cnvex 7863 . . . . . . . . . 10 ◑𝑓 ∈ V
7271imaex 7854 . . . . . . . . 9 (◑𝑓 β€œ 𝑧) ∈ V
7372elpw 4565 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ↔ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
74 breq1 5109 . . . . . . . . 9 (π‘₯ = (◑𝑓 β€œ 𝑧) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7572, 74elab 3631 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
7673, 75anbi12i 628 . . . . . . 7 (((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7770, 76bitri 275 . . . . . 6 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7863, 69, 773imtr4g 296 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
79 simpl 484 . . . . . . . . . . 11 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 ∈ 𝒫 𝐡)
8079elpwid 4570 . . . . . . . . . 10 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
8164, 80sylbi 216 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
82 imaeq2 6010 . . . . . . . . . . . 12 (𝑦 = (◑𝑓 β€œ 𝑧) β†’ (𝑓 β€œ 𝑦) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
83 f1orel 6788 . . . . . . . . . . . . . . . 16 (𝑓:𝐴–1-1-onto→𝐡 β†’ Rel 𝑓)
84 dfrel2 6142 . . . . . . . . . . . . . . . 16 (Rel 𝑓 ↔ ◑◑𝑓 = 𝑓)
8583, 84sylib 217 . . . . . . . . . . . . . . 15 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑◑𝑓 = 𝑓)
8685imaeq1d 6013 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8786adantr 482 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8846, 47syl 17 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1→𝐴)
89 f1imacnv 6801 . . . . . . . . . . . . . 14 ((◑𝑓:𝐡–1-1→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9088, 89sylan 581 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9187, 90eqtr3d 2775 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9282, 91sylan9eqr 2795 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ (𝑓 β€œ 𝑦) = 𝑧)
9392eqcomd 2739 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ 𝑧 = (𝑓 β€œ 𝑦))
9493ex 414 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9581, 94sylan2 594 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9695adantrl 715 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
97 simpl 484 . . . . . . . . . . 11 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 ∈ 𝒫 𝐴)
9897elpwid 4570 . . . . . . . . . 10 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
9932, 98sylbi 216 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
100 imaeq2 6010 . . . . . . . . . . . 12 (𝑧 = (𝑓 β€œ 𝑦) β†’ (◑𝑓 β€œ 𝑧) = (◑𝑓 β€œ (𝑓 β€œ 𝑦)))
101 f1imacnv 6801 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
10217, 101sylan 581 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
103100, 102sylan9eqr 2795 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ (◑𝑓 β€œ 𝑧) = 𝑦)
104103eqcomd 2739 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ 𝑦 = (◑𝑓 β€œ 𝑧))
105104ex 414 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10699, 105sylan2 594 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
107106adantrr 716 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10896, 107impbid 211 . . . . . 6 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦)))
109108ex 414 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦))))
1108, 16, 45, 78, 109en3d 8932 . . . 4 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
111110exlimiv 1934 . . 3 (βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
1121, 111sylbi 216 . 2 (𝐴 β‰ˆ 𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
113 df-pw 4563 . . . 4 𝒫 𝐴 = {π‘₯ ∣ π‘₯ βŠ† 𝐴}
114113ineq1i 4169 . . 3 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
115 inab 4260 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
116114, 115eqtri 2761 . 2 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
117 df-pw 4563 . . . 4 𝒫 𝐡 = {π‘₯ ∣ π‘₯ βŠ† 𝐡}
118117ineq1i 4169 . . 3 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
119 inab 4260 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
120118, 119eqtri 2761 . 2 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
121112, 116, 1203brtr3g 5139 1 (𝐴 β‰ˆ 𝐡 β†’ {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)} β‰ˆ {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710  Vcvv 3444   ∩ cin 3910   βŠ† wss 3911  π’« cpw 4561   class class class wbr 5106  β—‘ccnv 5633  dom cdm 5634  ran crn 5635   β€œ cima 5637  Rel wrel 5639  β€“1-1β†’wf1 6494  β€“ontoβ†’wfo 6495  β€“1-1-ontoβ†’wf1o 6496   β‰ˆ cen 8883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-er 8651  df-en 8887
This theorem is referenced by:  infmap2  10159
  Copyright terms: Public domain W3C validator