ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssenen GIF version
Theorem ssenen 6851
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 6747 . . 3 (𝐴 β‰ˆ 𝐡 ↔ βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡)
2 f1odm 5466 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ dom 𝑓 = 𝐴)
3 vex 2741 . . . . . . . 8 𝑓 ∈ V
43dmex 4894 . . . . . . 7 dom 𝑓 ∈ V
52, 4eqeltrrdi 2269 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐴 ∈ V)
6 pwexg 4181 . . . . . 6 (𝐴 ∈ V β†’ 𝒫 𝐴 ∈ V)
7 inex1g 4140 . . . . . 6 (𝒫 𝐴 ∈ V β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
85, 6, 73syl 17 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
9 f1ofo 5469 . . . . . . . 8 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–onto→𝐡)
10 forn 5442 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ ran 𝑓 = 𝐡)
119, 10syl 14 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ran 𝑓 = 𝐡)
123rnex 4895 . . . . . . 7 ran 𝑓 ∈ V
1311, 12eqeltrrdi 2269 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝐡 ∈ V)
14 pwexg 4181 . . . . . 6 (𝐡 ∈ V β†’ 𝒫 𝐡 ∈ V)
15 inex1g 4140 . . . . . 6 (𝒫 𝐡 ∈ V β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
1613, 14, 153syl 17 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∈ V)
17 f1of1 5461 . . . . . . . . . . 11 (𝑓:𝐴–1-1-onto→𝐡 β†’ 𝑓:𝐴–1-1→𝐡)
1817adantr 276 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑓:𝐴–1-1→𝐡)
1913adantr 276 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝐡 ∈ V)
20 simpr 110 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 βŠ† 𝐴)
21 vex 2741 . . . . . . . . . . 11 𝑦 ∈ V
2221a1i 9 . . . . . . . . . 10 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 ∈ V)
23 f1imaen2g 6793 . . . . . . . . . 10 (((𝑓:𝐴–1-1→𝐡 ∧ 𝐡 ∈ V) ∧ (𝑦 βŠ† 𝐴 ∧ 𝑦 ∈ V)) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
2418, 19, 20, 22, 23syl22anc 1239 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝑦)
25 entr 6784 . . . . . . . . 9 (((𝑓 β€œ 𝑦) β‰ˆ 𝑦 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2624, 25sylan 283 . . . . . . . 8 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
2726expl 378 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
28 imassrn 4982 . . . . . . . . 9 (𝑓 β€œ 𝑦) βŠ† ran 𝑓
2928, 10sseqtrid 3206 . . . . . . . 8 (𝑓:𝐴–onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
309, 29syl 14 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑓 β€œ 𝑦) βŠ† 𝐡)
3127, 30jctild 316 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢) β†’ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)))
32 elin 3319 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
3321elpw 3582 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 βŠ† 𝐴)
34 breq1 4007 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑦 β‰ˆ 𝐢))
3521, 34elab 2882 . . . . . . . 8 (𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑦 β‰ˆ 𝐢)
3633, 35anbi12i 460 . . . . . . 7 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
3732, 36bitri 184 . . . . . 6 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑦 βŠ† 𝐴 ∧ 𝑦 β‰ˆ 𝐢))
38 elin 3319 . . . . . . 7 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
393imaex 4984 . . . . . . . . 9 (𝑓 β€œ 𝑦) ∈ V
4039elpw 3582 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ↔ (𝑓 β€œ 𝑦) βŠ† 𝐡)
41 breq1 4007 . . . . . . . . 9 (π‘₯ = (𝑓 β€œ 𝑦) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4239, 41elab 2882 . . . . . . . 8 ((𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (𝑓 β€œ 𝑦) β‰ˆ 𝐢)
4340, 42anbi12i 460 . . . . . . 7 (((𝑓 β€œ 𝑦) ∈ 𝒫 𝐡 ∧ (𝑓 β€œ 𝑦) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4438, 43bitri 184 . . . . . 6 ((𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((𝑓 β€œ 𝑦) βŠ† 𝐡 ∧ (𝑓 β€œ 𝑦) β‰ˆ 𝐢))
4531, 37, 443imtr4g 205 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (𝑓 β€œ 𝑦) ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
46 f1ocnv 5475 . . . . . . 7 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1-onto→𝐴)
47 f1of1 5461 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1→𝐴)
48 f1f1orn 5473 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1→𝐴 β†’ ◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓)
49 f1of1 5461 . . . . . . . . . . . 12 (◑𝑓:𝐡–1-1-ontoβ†’ran ◑𝑓 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
5047, 48, 493syl 17 . . . . . . . . . . 11 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–1-1β†’ran ◑𝑓)
51 vex 2741 . . . . . . . . . . . 12 𝑧 ∈ V
5251f1imaen 6794 . . . . . . . . . . 11 ((◑𝑓:𝐡–1-1β†’ran ◑𝑓 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
5350, 52sylan 283 . . . . . . . . . 10 ((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝑧)
54 entr 6784 . . . . . . . . . 10 (((◑𝑓 β€œ 𝑧) β‰ˆ 𝑧 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5553, 54sylan 283 . . . . . . . . 9 (((◑𝑓:𝐡–1-1-onto→𝐴 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
5655expl 378 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
57 f1ofo 5469 . . . . . . . . 9 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ◑𝑓:𝐡–onto→𝐴)
58 imassrn 4982 . . . . . . . . . 10 (◑𝑓 β€œ 𝑧) βŠ† ran ◑𝑓
59 forn 5442 . . . . . . . . . 10 (◑𝑓:𝐡–onto→𝐴 β†’ ran ◑𝑓 = 𝐴)
6058, 59sseqtrid 3206 . . . . . . . . 9 (◑𝑓:𝐡–onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6157, 60syl 14 . . . . . . . 8 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
6256, 61jctild 316 . . . . . . 7 (◑𝑓:𝐡–1-1-onto→𝐴 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
6346, 62syl 14 . . . . . 6 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢) β†’ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)))
64 elin 3319 . . . . . . 7 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
6551elpw 3582 . . . . . . . 8 (𝑧 ∈ 𝒫 𝐡 ↔ 𝑧 βŠ† 𝐡)
66 breq1 4007 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (π‘₯ β‰ˆ 𝐢 ↔ 𝑧 β‰ˆ 𝐢))
6751, 66elab 2882 . . . . . . . 8 (𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ 𝑧 β‰ˆ 𝐢)
6865, 67anbi12i 460 . . . . . . 7 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
6964, 68bitri 184 . . . . . 6 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ (𝑧 βŠ† 𝐡 ∧ 𝑧 β‰ˆ 𝐢))
70 elin 3319 . . . . . . 7 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
713cnvex 5168 . . . . . . . . . 10 ◑𝑓 ∈ V
7271imaex 4984 . . . . . . . . 9 (◑𝑓 β€œ 𝑧) ∈ V
7372elpw 3582 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ↔ (◑𝑓 β€œ 𝑧) βŠ† 𝐴)
74 breq1 4007 . . . . . . . . 9 (π‘₯ = (◑𝑓 β€œ 𝑧) β†’ (π‘₯ β‰ˆ 𝐢 ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7572, 74elab 2882 . . . . . . . 8 ((◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢} ↔ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢)
7673, 75anbi12i 460 . . . . . . 7 (((◑𝑓 β€œ 𝑧) ∈ 𝒫 𝐴 ∧ (◑𝑓 β€œ 𝑧) ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7770, 76bitri 184 . . . . . 6 ((◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ↔ ((◑𝑓 β€œ 𝑧) βŠ† 𝐴 ∧ (◑𝑓 β€œ 𝑧) β‰ˆ 𝐢))
7863, 69, 773imtr4g 205 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ (◑𝑓 β€œ 𝑧) ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})))
79 simpl 109 . . . . . . . . . . 11 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 ∈ 𝒫 𝐡)
8079elpwid 3587 . . . . . . . . . 10 ((𝑧 ∈ 𝒫 𝐡 ∧ 𝑧 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
8164, 80sylbi 121 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑧 βŠ† 𝐡)
82 imaeq2 4967 . . . . . . . . . . . 12 (𝑦 = (◑𝑓 β€œ 𝑧) β†’ (𝑓 β€œ 𝑦) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
83 f1orel 5465 . . . . . . . . . . . . . . . 16 (𝑓:𝐴–1-1-onto→𝐡 β†’ Rel 𝑓)
84 dfrel2 5080 . . . . . . . . . . . . . . . 16 (Rel 𝑓 ↔ ◑◑𝑓 = 𝑓)
8583, 84sylib 122 . . . . . . . . . . . . . . 15 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑◑𝑓 = 𝑓)
8685imaeq1d 4970 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8786adantr 276 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = (𝑓 β€œ (◑𝑓 β€œ 𝑧)))
8846, 47syl 14 . . . . . . . . . . . . . 14 (𝑓:𝐴–1-1-onto→𝐡 β†’ ◑𝑓:𝐡–1-1→𝐴)
89 f1imacnv 5479 . . . . . . . . . . . . . 14 ((◑𝑓:𝐡–1-1→𝐴 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9088, 89sylan 283 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (◑◑𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9187, 90eqtr3d 2212 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑓 β€œ (◑𝑓 β€œ 𝑧)) = 𝑧)
9282, 91sylan9eqr 2232 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ (𝑓 β€œ 𝑦) = 𝑧)
9392eqcomd 2183 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) ∧ 𝑦 = (◑𝑓 β€œ 𝑧)) β†’ 𝑧 = (𝑓 β€œ 𝑦))
9493ex 115 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 βŠ† 𝐡) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9581, 94sylan2 286 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
9695adantrl 478 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) β†’ 𝑧 = (𝑓 β€œ 𝑦)))
97 simpl 109 . . . . . . . . . . 11 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 ∈ 𝒫 𝐴)
9897elpwid 3587 . . . . . . . . . 10 ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
9932, 98sylbi 121 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β†’ 𝑦 βŠ† 𝐴)
100 imaeq2 4967 . . . . . . . . . . . 12 (𝑧 = (𝑓 β€œ 𝑦) β†’ (◑𝑓 β€œ 𝑧) = (◑𝑓 β€œ (𝑓 β€œ 𝑦)))
101 f1imacnv 5479 . . . . . . . . . . . . 13 ((𝑓:𝐴–1-1→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
10217, 101sylan 283 . . . . . . . . . . . 12 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (◑𝑓 β€œ (𝑓 β€œ 𝑦)) = 𝑦)
103100, 102sylan9eqr 2232 . . . . . . . . . . 11 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ (◑𝑓 β€œ 𝑧) = 𝑦)
104103eqcomd 2183 . . . . . . . . . 10 (((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) ∧ 𝑧 = (𝑓 β€œ 𝑦)) β†’ 𝑦 = (◑𝑓 β€œ 𝑧))
105104ex 115 . . . . . . . . 9 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 βŠ† 𝐴) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10699, 105sylan2 286 . . . . . . . 8 ((𝑓:𝐴–1-1-onto→𝐡 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
107106adantrr 479 . . . . . . 7 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑧 = (𝑓 β€œ 𝑦) β†’ 𝑦 = (◑𝑓 β€œ 𝑧)))
10896, 107impbid 129 . . . . . 6 ((𝑓:𝐴–1-1-onto→𝐡 ∧ (𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦)))
109108ex 115 . . . . 5 (𝑓:𝐴–1-1-onto→𝐡 β†’ ((𝑦 ∈ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) ∧ 𝑧 ∈ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})) β†’ (𝑦 = (◑𝑓 β€œ 𝑧) ↔ 𝑧 = (𝑓 β€œ 𝑦))))
1108, 16, 45, 78, 109en3d 6769 . . . 4 (𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
111110exlimiv 1598 . . 3 (βˆƒπ‘“ 𝑓:𝐴–1-1-onto→𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
1121, 111sylbi 121 . 2 (𝐴 β‰ˆ 𝐡 β†’ (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) β‰ˆ (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}))
113 df-pw 3578 . . . 4 𝒫 𝐴 = {π‘₯ ∣ π‘₯ βŠ† 𝐴}
114113ineq1i 3333 . . 3 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
115 inab 3404 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐴} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
116114, 115eqtri 2198 . 2 (𝒫 𝐴 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)}
117 df-pw 3578 . . . 4 𝒫 𝐡 = {π‘₯ ∣ π‘₯ βŠ† 𝐡}
118117ineq1i 3333 . . 3 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢})
119 inab 3404 . . 3 ({π‘₯ ∣ π‘₯ βŠ† 𝐡} ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
120118, 119eqtri 2198 . 2 (𝒫 𝐡 ∩ {π‘₯ ∣ π‘₯ β‰ˆ 𝐢}) = {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)}
121112, 116, 1203brtr3g 4037 1 (𝐴 β‰ˆ 𝐡 β†’ {π‘₯ ∣ (π‘₯ βŠ† 𝐴 ∧ π‘₯ β‰ˆ 𝐢)} β‰ˆ {π‘₯ ∣ (π‘₯ βŠ† 𝐡 ∧ π‘₯ β‰ˆ 𝐢)})
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353  βˆƒwex 1492   ∈ wcel 2148  {cab 2163  Vcvv 2738   ∩ cin 3129   βŠ† wss 3130  π’« cpw 3576   class class class wbr 4004  β—‘ccnv 4626  dom cdm 4627  ran crn 4628   β€œ cima 4630  Rel wrel 4632  β€“1-1β†’wf1 5214  β€“ontoβ†’wfo 5215  β€“1-1-ontoβ†’wf1o 5216   β‰ˆ cen 6738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-er 6535  df-en 6741
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator