Metamath Proof Explorer

Theorem sticksstones4

Description: Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024)

Ref Expression
Hypotheses sticksstones4.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones4.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
sticksstones4.3 ⊢ 𝐵 = { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 }
sticksstones4.4 ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
Assertion sticksstones4 ( 𝜑 → 𝐴 ≈ 𝐵 )

Proof

Step Hyp Ref Expression
1 sticksstones4.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones4.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones4.3 ⊢ 𝐵 = { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 }
4 sticksstones4.4 ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
5 eqid ⊢ ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) = ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 )
6 1 2 3 4 5 sticksstones2 ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1→ 𝐵 )
7 1 2 3 4 5 sticksstones3 ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –onto→ 𝐵 )
8 6 7 jca ⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1→ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –onto→ 𝐵 ) )
9 df-f1o ⊢ ( ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1-onto→ 𝐵 ↔ ( ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1→ 𝐵 ∧ ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –onto→ 𝐵 ) )
10 8 9 sylibr ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1-onto→ 𝐵 )
11 simpl ⊢ ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
12 11 a1i ⊢ ( 𝜑 → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ) )
13 12 ss2abdv ⊢ ( 𝜑 → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) } )
14 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐾 ) ∈ Fin )
15 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
16 mapex ⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) } ∈ V )
17 14 15 16 syl2anc ⊢ ( 𝜑 → { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) } ∈ V )
18 ssexg ⊢ ( ( { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) } ∧ { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) } ∈ V ) → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V )
19 13 17 18 syl2anc ⊢ ( 𝜑 → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V )
20 4 eleq1i ⊢ ( 𝐴 ∈ V ↔ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V )
21 19 20 sylibr ⊢ ( 𝜑 → 𝐴 ∈ V )
22 21 mptexd ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) ∈ V )
23 f1oeq1 ⊢ ( 𝑔 = ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) → ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1-onto→ 𝐵 ) )
24 23 biimprd ⊢ ( 𝑔 = ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) → ( ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1-onto→ 𝐵 → 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑔 = ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) ) → ( ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1-onto→ 𝐵 → 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) )
26 22 25 spcimedv ⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐴 ↦ ran 𝑝 ) : 𝐴 –1-1-onto→ 𝐵 → ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) )
27 10 26 mpd ⊢ ( 𝜑 → ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 )
28 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 )
29 27 28 sylibr ⊢ ( 𝜑 → 𝐴 ≈ 𝐵 )