Metamath Proof Explorer


Theorem fodomacn

Description: A version of fodom that doesn't require the Axiom of Choice ax-ac . If A has choice sequences of length B , then any surjection from A to B can be inverted to an injection the other way. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion fodomacn ( 𝐴AC 𝐵 → ( 𝐹 : 𝐴onto𝐵𝐵𝐴 ) )

Proof

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𝐵𝐵𝐴 ) )