Step |
Hyp |
Ref |
Expression |
1 |
|
indf1o |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) ) |
2 |
|
f1of1 |
⊢ ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1→ ( { 0 , 1 } ↑m 𝑂 ) ) |
3 |
1 2
|
syl |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1→ ( { 0 , 1 } ↑m 𝑂 ) ) |
4 |
|
inss1 |
⊢ ( 𝒫 𝑂 ∩ Fin ) ⊆ 𝒫 𝑂 |
5 |
|
f1ores |
⊢ ( ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1→ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( 𝒫 𝑂 ∩ Fin ) ⊆ 𝒫 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ) |
6 |
3 4 5
|
sylancl |
⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ) |
7 |
|
resres |
⊢ ( ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) ↾ Fin ) = ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) |
8 |
|
f1ofn |
⊢ ( ( 𝟭 ‘ 𝑂 ) : 𝒫 𝑂 –1-1-onto→ ( { 0 , 1 } ↑m 𝑂 ) → ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 ) |
9 |
|
fnresdm |
⊢ ( ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 → ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) = ( 𝟭 ‘ 𝑂 ) ) |
10 |
1 8 9
|
3syl |
⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) = ( 𝟭 ‘ 𝑂 ) ) |
11 |
10
|
reseq1d |
⊢ ( 𝑂 ∈ 𝑉 → ( ( ( 𝟭 ‘ 𝑂 ) ↾ 𝒫 𝑂 ) ↾ Fin ) = ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) ) |
12 |
7 11
|
eqtr3id |
⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) = ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) ) |
13 |
|
eqidd |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝒫 𝑂 ∩ Fin ) = ( 𝒫 𝑂 ∩ Fin ) ) |
14 |
|
simpll |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → 𝑂 ∈ 𝑉 ) |
15 |
|
simpr |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) |
16 |
4 15
|
sselid |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎 ∈ 𝒫 𝑂 ) |
17 |
16
|
elpwid |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎 ⊆ 𝑂 ) |
18 |
|
indf |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } ) |
19 |
17 18
|
syldan |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } ) |
20 |
19
|
adantr |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } ) |
21 |
|
simpr |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) |
22 |
21
|
feq1d |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) : 𝑂 ⟶ { 0 , 1 } ↔ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) ) |
23 |
20 22
|
mpbid |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → 𝑔 : 𝑂 ⟶ { 0 , 1 } ) |
24 |
|
prex |
⊢ { 0 , 1 } ∈ V |
25 |
|
elmapg |
⊢ ( ( { 0 , 1 } ∈ V ∧ 𝑂 ∈ 𝑉 ) → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ↔ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) ) |
26 |
24 25
|
mpan |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ↔ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) ) |
27 |
26
|
biimpar |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) → 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) |
28 |
14 23 27
|
syl2anc |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) |
29 |
21
|
cnveqd |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = ◡ 𝑔 ) |
30 |
29
|
imaeq1d |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) = ( ◡ 𝑔 “ { 1 } ) ) |
31 |
|
indpi1 |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) = 𝑎 ) |
32 |
17 31
|
syldan |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) = 𝑎 ) |
33 |
|
inss2 |
⊢ ( 𝒫 𝑂 ∩ Fin ) ⊆ Fin |
34 |
33 15
|
sselid |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → 𝑎 ∈ Fin ) |
35 |
32 34
|
eqeltrd |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) ∈ Fin ) |
36 |
35
|
adantr |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) “ { 1 } ) ∈ Fin ) |
37 |
30 36
|
eqeltrrd |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) |
38 |
28 37
|
jca |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) |
39 |
38
|
rexlimdva2 |
⊢ ( 𝑂 ∈ 𝑉 → ( ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 → ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) ) |
40 |
|
cnvimass |
⊢ ( ◡ 𝑔 “ { 1 } ) ⊆ dom 𝑔 |
41 |
26
|
biimpa |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) → 𝑔 : 𝑂 ⟶ { 0 , 1 } ) |
42 |
41
|
fdmd |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) → dom 𝑔 = 𝑂 ) |
43 |
42
|
adantrr |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) → dom 𝑔 = 𝑂 ) |
44 |
40 43
|
sseqtrid |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) → ( ◡ 𝑔 “ { 1 } ) ⊆ 𝑂 ) |
45 |
|
simprr |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) → ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) |
46 |
|
elfpw |
⊢ ( ( ◡ 𝑔 “ { 1 } ) ∈ ( 𝒫 𝑂 ∩ Fin ) ↔ ( ( ◡ 𝑔 “ { 1 } ) ⊆ 𝑂 ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) |
47 |
44 45 46
|
sylanbrc |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) → ( ◡ 𝑔 “ { 1 } ) ∈ ( 𝒫 𝑂 ∩ Fin ) ) |
48 |
|
indpreima |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) → 𝑔 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝑔 “ { 1 } ) ) ) |
49 |
48
|
eqcomd |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑔 : 𝑂 ⟶ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝑔 “ { 1 } ) ) = 𝑔 ) |
50 |
41 49
|
syldan |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝑔 “ { 1 } ) ) = 𝑔 ) |
51 |
50
|
adantrr |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝑔 “ { 1 } ) ) = 𝑔 ) |
52 |
|
fveqeq2 |
⊢ ( 𝑎 = ( ◡ 𝑔 “ { 1 } ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ↔ ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝑔 “ { 1 } ) ) = 𝑔 ) ) |
53 |
52
|
rspcev |
⊢ ( ( ( ◡ 𝑔 “ { 1 } ) ∈ ( 𝒫 𝑂 ∩ Fin ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝑔 “ { 1 } ) ) = 𝑔 ) → ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) |
54 |
47 51 53
|
syl2anc |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) → ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) |
55 |
54
|
ex |
⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) → ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) ) |
56 |
39 55
|
impbid |
⊢ ( 𝑂 ∈ 𝑉 → ( ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ↔ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) ) |
57 |
1 8
|
syl |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 ) |
58 |
|
fvelimab |
⊢ ( ( ( 𝟭 ‘ 𝑂 ) Fn 𝒫 𝑂 ∧ ( 𝒫 𝑂 ∩ Fin ) ⊆ 𝒫 𝑂 ) → ( 𝑔 ∈ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) ) |
59 |
57 4 58
|
sylancl |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝑔 ∈ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝑂 ∩ Fin ) ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑎 ) = 𝑔 ) ) |
60 |
|
cnveq |
⊢ ( 𝑓 = 𝑔 → ◡ 𝑓 = ◡ 𝑔 ) |
61 |
60
|
imaeq1d |
⊢ ( 𝑓 = 𝑔 → ( ◡ 𝑓 “ { 1 } ) = ( ◡ 𝑔 “ { 1 } ) ) |
62 |
61
|
eleq1d |
⊢ ( 𝑓 = 𝑔 → ( ( ◡ 𝑓 “ { 1 } ) ∈ Fin ↔ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) |
63 |
62
|
elrab |
⊢ ( 𝑔 ∈ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( ◡ 𝑓 “ { 1 } ) ∈ Fin } ↔ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) |
64 |
63
|
a1i |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝑔 ∈ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( ◡ 𝑓 “ { 1 } ) ∈ Fin } ↔ ( 𝑔 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∧ ( ◡ 𝑔 “ { 1 } ) ∈ Fin ) ) ) |
65 |
56 59 64
|
3bitr4d |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝑔 ∈ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ 𝑔 ∈ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( ◡ 𝑓 “ { 1 } ) ∈ Fin } ) ) |
66 |
65
|
eqrdv |
⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) = { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( ◡ 𝑓 “ { 1 } ) ∈ Fin } ) |
67 |
12 13 66
|
f1oeq123d |
⊢ ( 𝑂 ∈ 𝑉 → ( ( ( 𝟭 ‘ 𝑂 ) ↾ ( 𝒫 𝑂 ∩ Fin ) ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ ( ( 𝟭 ‘ 𝑂 ) “ ( 𝒫 𝑂 ∩ Fin ) ) ↔ ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( ◡ 𝑓 “ { 1 } ) ∈ Fin } ) ) |
68 |
6 67
|
mpbid |
⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ↾ Fin ) : ( 𝒫 𝑂 ∩ Fin ) –1-1-onto→ { 𝑓 ∈ ( { 0 , 1 } ↑m 𝑂 ) ∣ ( ◡ 𝑓 “ { 1 } ) ∈ Fin } ) |