MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssenen Structured version   Visualization version   GIF version
Theorem ssenen 9180
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 8978 . . 3 (𝐴 β‰ˆ 𝐡 ↔ βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡)
2 f1odm 6846 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ dom 𝑓 = 𝐴)
3 vex 3475 . . . . . . . 8 𝑓 ∈ V
43dmex 7921 . . . . . . 7 dom 𝑓 ∈ V
52, 4eqeltrrdi 2837 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐴 ∈ V)
6 pwexg 5380 . . . . . 6 (𝐴 ∈ V β†’ 𝒫 𝐴 ∈ V)
7 inex1g 5321 . . . . . 6 (𝒫 𝐴 ∈ V β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
85, 6, 73syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
9 f1ofo 6849 . . . . . . . 8 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–onto→𝐡)
10 forn 6817 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ ran 𝑓 = 𝐡)
119, 10syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ran 𝑓 = 𝐡)
123rnex 7922 . . . . . . 7 ran 𝑓 ∈ V
1311, 12eqeltrrdi 2837 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐡 ∈ V)
14 pwexg 5380 . . . . . 6 (𝐡 ∈ V β†’ 𝒫 𝐡 ∈ V)
15 inex1g 5321 . . . . . 6 (𝒫 𝐡 ∈ V β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
1613, 14, 153syl 18 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
17 f1of1 6841 . . . . . . . . . . 11 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–1-1→𝐡)
1817adantr 479 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑓:𝐴–1-1→𝐡)
1913adantr 479 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝐡 ∈ V)
20 simpr 483 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 βŠ† 𝐴)
21 vex 3475 . . . . . . . . . . 11 𝑦 ∈ V
2221a1i 11 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 ∈ V)
23 f1imaen2g 9040 . . . . . . . . . 10 (((𝑓:𝐴–1-1→𝐡 ∧ 𝐡 ∈ V) ∧ (𝑦 βŠ† 𝐴 ∧ 𝑦 ∈ V)) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
2418, 19, 20, 22, 23syl22anc 837 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
25 entr 9031 . . . . . . . . 9 (((𝑓 β€œ 𝑦) β‰ˆ 𝑦 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2624, 25sylan 578 . . . . . . . 8 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2726expl 456 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
28 imassrn 6077 . . . . . . . . 9 (𝑓 β€œ 𝑦) βŠ† ran 𝑓
2928, 10sseqtrid 4032 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
309, 29syl 17 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
3127, 30jctild 524 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)))
32 elin 3963 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
3321elpw 4608 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 βŠ† 𝐴)
34 breq1 5153 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑦 β‰ˆ 𝐢))
3521, 34elab 3667 . . . . . . . 8 (𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑦 β‰ˆ 𝐢)
3633, 35anbi12i 626 . . . . . . 7 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
3732, 36bitri 274 . . . . . 6 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
38 elin 3963 . . . . . . 7 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
393imaex 7926 . . . . . . . . 9 (𝑓 β€œ 𝑦) ∈ V
4039elpw 4608 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ↔ (𝑓 β€œ 𝑦) βŠ† 𝐡)
41 breq1 5153 . . . . . . . . 9 (π‘₯ = (𝑓 β€œ 𝑦) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4239, 41elab 3667 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
4340, 42anbi12i 626 . . . . . . 7 (((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4438, 43bitri 274 . . . . . 6 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4531, 37, 443imtr4g 295 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
46 f1ocnv 6854 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1-onto→𝐴)
47 f1of1 6841 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1→𝐴)
48 f1f1orn 6853 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1→𝐴 β†’ ◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓)
49 f1of1 6841 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
5047, 48, 493syl 18 . . . . . . . . . . 11 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
51 vex 3475 . . . . . . . . . . . 12 𝑧 ∈ V
5251f1imaen 9041 . . . . . . . . . . 11 ((◑𝑓:𝐡–1-1β†’ran ◑𝑓 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
5350, 52sylan 578 . . . . . . . . . 10 ((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
54 entr 9031 . . . . . . . . . 10 (((◑𝑓 β€œ 𝑧) β‰ˆ 𝑧 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5553, 54sylan 578 . . . . . . . . 9 (((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5655expl 456 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
57 f1ofo 6849 . . . . . . . . 9 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–onto→𝐴)
58 imassrn 6077 . . . . . . . . . 10 (◑𝑓 β€œ 𝑧) βŠ† ran ◑𝑓
59 forn 6817 . . . . . . . . . 10 (◑𝑓:𝐡–onto→𝐴 β†’ ran ◑𝑓 = 𝐴)
6058, 59sseqtrid 4032 . . . . . . . . 9 (◑𝑓:𝐡–onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6157, 60syl 17 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6256, 61jctild 524 . . . . . . 7 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
6346, 62syl 17 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
64 elin 3963 . . . . . . 7 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
6551elpw 4608 . . . . . . . 8 (𝑧 ∈ 𝒫 𝐡 ↔ 𝑧 βŠ† 𝐡)
66 breq1 5153 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑧 β‰ˆ 𝐢))
6751, 66elab 3667 . . . . . . . 8 (𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑧 β‰ˆ 𝐢)
6865, 67anbi12i 626 . . . . . . 7 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
6964, 68bitri 274 . . . . . 6 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
70 elin 3963 . . . . . . 7 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
713cnvex 7937 . . . . . . . . . 10 ◑𝑓 ∈ V
7271imaex 7926 . . . . . . . . 9 (◑𝑓 β€œ 𝑧) ∈ V
7372elpw 4608 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ↔ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
74 breq1 5153 . . . . . . . . 9 (π‘₯ = (◑𝑓 β€œ 𝑧) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7572, 74elab 3667 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
7673, 75anbi12i 626 . . . . . . 7 (((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7770, 76bitri 274 . . . . . 6 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7863, 69, 773imtr4g 295 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
79 simpl 481 . . . . . . . . . . 11 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 ∈ 𝒫 𝐡)
8079elpwid 4613 . . . . . . . . . 10 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
8164, 80sylbi 216 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
82 imaeq2 6062 . . . . . . . . . . . 12 (𝑦 = (◑𝑓 β€œ 𝑧) β†’ (𝑓 β€œ 𝑦) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
83 f1orel 6845 . . . . . . . . . . . . . . . 16 (𝑓:𝐴–1-1-onto→𝐡 β†’ Rel 𝑓)
84 dfrel2 6196 . . . . . . . . . . . . . . . 16 (Rel 𝑓 ↔ ◑◑𝑓 = 𝑓)
8583, 84sylib 217 . . . . . . . . . . . . . . 15 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑◑𝑓 = 𝑓)
8685imaeq1d 6065 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8786adantr 479 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8846, 47syl 17 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1→𝐴)
89 f1imacnv 6858 . . . . . . . . . . . . . 14 ((◑𝑓:𝐡–1-1→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9088, 89sylan 578 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9187, 90eqtr3d 2769 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9282, 91sylan9eqr 2789 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ (𝑓 β€œ 𝑦) = 𝑧)
9392eqcomd 2733 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ 𝑧 = (𝑓 β€œ 𝑦))
9493ex 411 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9581, 94sylan2 591 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9695adantrl 714 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
97 simpl 481 . . . . . . . . . . 11 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 ∈ 𝒫 𝐴)
9897elpwid 4613 . . . . . . . . . 10 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
9932, 98sylbi 216 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
100 imaeq2 6062 . . . . . . . . . . . 12 (𝑧 = (𝑓 β€œ 𝑦) β†’ (◑𝑓 β€œ 𝑧) = (◑𝑓 β€œ (𝑓 β€œ 𝑦)))
101 f1imacnv 6858 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
10217, 101sylan 578 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
103100, 102sylan9eqr 2789 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ (◑𝑓 β€œ 𝑧) = 𝑦)
104103eqcomd 2733 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ 𝑦 = (◑𝑓 β€œ 𝑧))
105104ex 411 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10699, 105sylan2 591 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
107106adantrr 715 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10896, 107impbid 211 . . . . . 6 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦)))
109108ex 411 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦))))
1108, 16, 45, 78, 109en3d 9014 . . . 4 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
111110exlimiv 1925 . . 3 (βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
1121, 111sylbi 216 . 2 (𝐴 β‰ˆ 𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
113 df-pw 4606 . . . 4 𝒫 𝐴 = {π‘₯ ∣ π‘₯ βŠ† 𝐴}
114113ineq1i 4208 . . 3 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
115 inab 4300 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
116114, 115eqtri 2755 . 2 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
117 df-pw 4606 . . . 4 𝒫 𝐡 = {π‘₯ ∣ π‘₯ βŠ† 𝐡}
118117ineq1i 4208 . . 3 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
119 inab 4300 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
120118, 119eqtri 2755 . 2 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
121112, 116, 1203brtr3g 5183 1 (𝐴 β‰ˆ 𝐡 β†’ {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)} β‰ˆ {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  {cab 2704  Vcvv 3471   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4604   class class class wbr 5150  β—‘ccnv 5679  dom cdm 5680  ran crn 5681   β€œ cima 5683  Rel wrel 5685  β€“1-1β†’wf1 6548  β€“ontoβ†’wfo 6549  β€“1-1-ontoβ†’wf1o 6550   β‰ˆ cen 8965
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 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-id 5578  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-er 8729  df-en 8969
This theorem is referenced by:  infmap2  10247
  Copyright terms: Public domain W3C validator