Step |
Hyp |
Ref |
Expression |
1 |
|
foelrn |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑦 ) ) |
2 |
1
|
ralrimiva |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑦 ) ) |
3 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) |
4 |
3
|
eqeq2d |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) |
5 |
4
|
acni3 |
⊢ ( ( 𝐴 ∈ AC 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) |
6 |
2 5
|
sylan2 |
⊢ ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) |
7 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝐴 ∈ AC 𝐵 ) |
8 |
|
acnrcl |
⊢ ( 𝐴 ∈ AC 𝐵 → 𝐵 ∈ V ) |
9 |
7 8
|
syl |
⊢ ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝐵 ∈ V ) |
10 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑓 : 𝐵 ⟶ 𝐴 ) |
11 |
|
fveq2 |
⊢ ( ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑧 ) → ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑧 ) ) ) |
12 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) |
13 |
|
id |
⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 ) |
14 |
|
2fveq3 |
⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) ) |
15 |
13 14
|
eqeq12d |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ 𝑦 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) ) ) |
16 |
15
|
rspccva |
⊢ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) ) |
17 |
|
id |
⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 ) |
18 |
|
2fveq3 |
⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑧 ) ) ) |
19 |
17 18
|
eqeq12d |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ 𝑧 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) |
20 |
19
|
rspccva |
⊢ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑧 ) ) ) |
21 |
16 20
|
eqeqan12d |
⊢ ( ( ( ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 = 𝑧 ↔ ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) |
22 |
21
|
anandis |
⊢ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 = 𝑧 ↔ ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) |
23 |
12 22
|
sylan |
⊢ ( ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 = 𝑧 ↔ ( 𝐹 ‘ ( 𝑓 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) |
24 |
11 23
|
syl5ibr |
⊢ ( ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) |
25 |
24
|
ralrimivva |
⊢ ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) |
26 |
|
dff13 |
⊢ ( 𝑓 : 𝐵 –1-1→ 𝐴 ↔ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) ) |
27 |
10 25 26
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑓 : 𝐵 –1-1→ 𝐴 ) |
28 |
|
f1dom2g |
⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ AC 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐴 ) → 𝐵 ≼ 𝐴 ) |
29 |
9 7 27 28
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝐵 ≼ 𝐴 ) |
30 |
6 29
|
exlimddv |
⊢ ( ( 𝐴 ∈ AC 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 ) |
31 |
30
|
ex |
⊢ ( 𝐴 ∈ AC 𝐵 → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 ) ) |