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 imbitrrid ⊢ ( ( ( ( 𝐴 ∈ 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→ 𝐵 → 𝐵 ≼ 𝐴 ) )