Step |
Hyp |
Ref |
Expression |
1 |
|
pautset.s |
⊢ 𝑆 = ( PSubSp ‘ 𝐾 ) |
2 |
|
pautset.m |
⊢ 𝑀 = ( PAut ‘ 𝐾 ) |
3 |
1 2
|
pautsetN |
⊢ ( 𝐾 ∈ 𝐵 → 𝑀 = { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } ) |
4 |
3
|
eleq2d |
⊢ ( 𝐾 ∈ 𝐵 → ( 𝐹 ∈ 𝑀 ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } ) ) |
5 |
|
f1of |
⊢ ( 𝐹 : 𝑆 –1-1-onto→ 𝑆 → 𝐹 : 𝑆 ⟶ 𝑆 ) |
6 |
1
|
fvexi |
⊢ 𝑆 ∈ V |
7 |
|
fex |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑆 ∧ 𝑆 ∈ V ) → 𝐹 ∈ V ) |
8 |
5 6 7
|
sylancl |
⊢ ( 𝐹 : 𝑆 –1-1-onto→ 𝑆 → 𝐹 ∈ V ) |
9 |
8
|
adantr |
⊢ ( ( 𝐹 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 ∈ V ) |
10 |
|
f1oeq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ↔ 𝐹 : 𝑆 –1-1-onto→ 𝑆 ) ) |
11 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
12 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
13 |
11 12
|
sseq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) |
14 |
13
|
bibi2d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) ) |
15 |
14
|
2ralbidv |
⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) ) |
16 |
10 15
|
anbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝐹 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
17 |
9 16
|
elab3 |
⊢ ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝐹 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) ) |
18 |
4 17
|
bitrdi |
⊢ ( 𝐾 ∈ 𝐵 → ( 𝐹 ∈ 𝑀 ↔ ( 𝐹 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) ) ) |