This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iundomg

Description: An upper bound for the cardinality of an indexed union, with explicit choice principles. B depends on x and should be thought of as B ( x ) . (Contributed by Mario Carneiro, 1-Sep-2015)

		Ref	Expression
	Hypotheses	iunfo.1	$⊢ T = ⋃_{x \in A} (\{x\} \times B)$
		iundomg.2	$⊢ φ \to ⋃_{x \in A} (C^{B}) \in \underline{AC} A$
		iundomg.3	$⊢ φ \to \forall x \in A B ≼ C$
		iundomg.4	$⊢ φ \to A \times C \in \underline{AC} ⋃_{x \in A} B$
	Assertion	iundomg	$⊢ φ \to ⋃_{x \in A} B ≼ (A \times C)$

Proof

Step	Hyp	Ref	Expression
1		iunfo.1	$⊢ T = ⋃_{x \in A} (\{x\} \times B)$
2		iundomg.2	$⊢ φ \to ⋃_{x \in A} (C^{B}) \in \underline{AC} A$
3		iundomg.3	$⊢ φ \to \forall x \in A B ≼ C$
4		iundomg.4	$⊢ φ \to A \times C \in \underline{AC} ⋃_{x \in A} B$
5	1 2 3	iundom2g	$⊢ φ \to T ≼ (A \times C)$
6		acndom2	$⊢ T ≼ (A \times C) \to (A \times C \in \underline{AC} ⋃_{x \in A} B \to T \in \underline{AC} ⋃_{x \in A} B)$
7	5 4 6	sylc	$⊢ φ \to T \in \underline{AC} ⋃_{x \in A} B$
8	1	iunfo	$⊢ ({2^{nd} ↾}_{T}) : T \underset{onto}{⟶} ⋃_{x \in A} B$
9		fodomacn	$⊢ T \in \underline{AC} ⋃_{x \in A} B \to (({2^{nd} ↾}_{T}) : T \underset{onto}{⟶} ⋃_{x \in A} B \to ⋃_{x \in A} B ≼ T)$
10	7 8 9	mpisyl	$⊢ φ \to ⋃_{x \in A} B ≼ T$
11		domtr	$⊢ (⋃_{x \in A} B ≼ T \land T ≼ (A \times C)) \to ⋃_{x \in A} B ≼ (A \times C)$
12	10 5 11	syl2anc	$⊢ φ \to ⋃_{x \in A} B ≼ (A \times C)$