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	$⊢ \underline{Ⅎ} x A$
	Assertion	mptctf	$⊢ A ≼ ω \to (x \in A ⟼ B) ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		mptctf.1	$⊢ \underline{Ⅎ} x A$
2		funmpt	$⊢ Fun (x \in A ⟼ B)$
3		ctex	$⊢ A ≼ ω \to A \in V$
4		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
5	4	dmmpt	$⊢ dom (x \in A ⟼ B) = \{x \in A \| B \in V\}$
6		df-rab	$⊢ \{x \in A \| B \in V\} = \{x \| (x \in A \land B \in V)\}$
7		simpl	$⊢ (x \in A \land B \in V) \to x \in A$
8	7	ss2abi	$⊢ \{x \| (x \in A \land B \in V)\} \subseteq \{x \| x \in A\}$
9	1	abid2f	$⊢ \{x \| x \in A\} = A$
10	8 9	sseqtri	$⊢ \{x \| (x \in A \land B \in V)\} \subseteq A$
11	6 10	eqsstri	$⊢ \{x \in A \| B \in V\} \subseteq A$
12	5 11	eqsstri	$⊢ dom (x \in A ⟼ B) \subseteq A$
13		ssdomg	$⊢ A \in V \to (dom (x \in A ⟼ B) \subseteq A \to dom (x \in A ⟼ B) ≼ A)$
14	3 12 13	mpisyl	$⊢ A ≼ ω \to dom (x \in A ⟼ B) ≼ A$
15		domtr	$⊢ (dom (x \in A ⟼ B) ≼ A \land A ≼ ω) \to dom (x \in A ⟼ B) ≼ ω$
16	14 15	mpancom	$⊢ A ≼ ω \to dom (x \in A ⟼ B) ≼ ω$
17		funfn	$⊢ Fun (x \in A ⟼ B) \leftrightarrow (x \in A ⟼ B) Fn dom (x \in A ⟼ B)$
18		fnct	$⊢ ((x \in A ⟼ B) Fn dom (x \in A ⟼ B) \land dom (x \in A ⟼ B) ≼ ω) \to (x \in A ⟼ B) ≼ ω$
19	17 18	sylanb	$⊢ (Fun (x \in A ⟼ B) \land dom (x \in A ⟼ B) ≼ ω) \to (x \in A ⟼ B) ≼ ω$
20	2 16 19	sylancr	$⊢ A ≼ ω \to (x \in A ⟼ B) ≼ ω$

Metamath Proof Explorer

Theorem mptctf

Proof