Metamath Proof Explorer

Theorem mptctf

Description: A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypothesis mptctf.1 ⊢ Ⅎ _ x A
Assertion mptctf ⊢ A ≼ ω → x ∈ A ⟼ B ≼ ω

Proof

Step Hyp Ref Expression
1 mptctf.1 ⊢ Ⅎ _ x A
2 funmpt ⊢ Fun ⁡ x ∈ A ⟼ B
3 ctex ⊢ A ≼ ω → A ∈ V
4 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
5 4 dmmpt ⊢ dom ⁡ x ∈ A ⟼ B = x ∈ A | B ∈ V
6 df-rab ⊢ x ∈ A | B ∈ V = x | x ∈ A ∧ B ∈ V
7 simpl ⊢ x ∈ A ∧ B ∈ V → x ∈ A
8 7 ss2abi ⊢ x | x ∈ A ∧ B ∈ V ⊆ x | x ∈ A
9 1 abid2f ⊢ x | x ∈ A = A
10 8 9 sseqtri ⊢ x | x ∈ A ∧ B ∈ V ⊆ A
11 6 10 eqsstri ⊢ x ∈ A | B ∈ V ⊆ A
12 5 11 eqsstri ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A
13 ssdomg ⊢ A ∈ V → dom ⁡ x ∈ A ⟼ B ⊆ A → dom ⁡ x ∈ A ⟼ B ≼ A
14 3 12 13 mpisyl ⊢ A ≼ ω → dom ⁡ x ∈ A ⟼ B ≼ A
15 domtr ⊢ dom ⁡ x ∈ A ⟼ B ≼ A ∧ A ≼ ω → dom ⁡ x ∈ A ⟼ B ≼ ω
16 14 15 mpancom ⊢ A ≼ ω → dom ⁡ x ∈ A ⟼ B ≼ ω
17 funfn ⊢ Fun ⁡ x ∈ A ⟼ B ↔ x ∈ A ⟼ B Fn dom ⁡ x ∈ A ⟼ B
18 fnct ⊢ x ∈ A ⟼ B Fn dom ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ≼ ω → x ∈ A ⟼ B ≼ ω
19 17 18 sylanb ⊢ Fun ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ≼ ω → x ∈ A ⟼ B ≼ ω
20 2 16 19 sylancr ⊢ A ≼ ω → x ∈ A ⟼ B ≼ ω