fseqdom

Description: One half of fseqen . (Contributed by Mario Carneiro, 18-Nov-2014)

		Ref	Expression
	Assertion	fseqdom	$⊢ A \in V \to (ω \times A) ≼ ⋃_{n \in ω} (A^{n})$

Proof

Step	Hyp	Ref	Expression
1		omex	$⊢ ω \in V$
2		ovex	$⊢ A^{n} \in V$
3	1 2	iunex	$⊢ ⋃_{n \in ω} (A^{n}) \in V$
4		xp1st	$⊢ x \in (ω \times A) \to 1^{st} (x) \in ω$
5		peano2	$⊢ 1^{st} (x) \in ω \to suc 1^{st} (x) \in ω$
6	4 5	syl	$⊢ x \in (ω \times A) \to suc 1^{st} (x) \in ω$
7		xp2nd	$⊢ x \in (ω \times A) \to 2^{nd} (x) \in A$
8		fconst6g	$⊢ 2^{nd} (x) \in A \to (suc 1^{st} (x) \times \{2^{nd} (x)\}) : suc 1^{st} (x) ⟶ A$
9	7 8	syl	$⊢ x \in (ω \times A) \to (suc 1^{st} (x) \times \{2^{nd} (x)\}) : suc 1^{st} (x) ⟶ A$
10	9	adantl	$⊢ (A \in V \land x \in (ω \times A)) \to (suc 1^{st} (x) \times \{2^{nd} (x)\}) : suc 1^{st} (x) ⟶ A$
11		elmapg	$⊢ (A \in V \land suc 1^{st} (x) \in ω) \to (suc 1^{st} (x) \times \{2^{nd} (x)\} \in (A^{suc 1^{st} (x)}) \leftrightarrow (suc 1^{st} (x) \times \{2^{nd} (x)\}) : suc 1^{st} (x) ⟶ A)$
12	6 11	sylan2	$⊢ (A \in V \land x \in (ω \times A)) \to (suc 1^{st} (x) \times \{2^{nd} (x)\} \in (A^{suc 1^{st} (x)}) \leftrightarrow (suc 1^{st} (x) \times \{2^{nd} (x)\}) : suc 1^{st} (x) ⟶ A)$
13	10 12	mpbird	$⊢ (A \in V \land x \in (ω \times A)) \to suc 1^{st} (x) \times \{2^{nd} (x)\} \in (A^{suc 1^{st} (x)})$
14		oveq2	$⊢ n = suc 1^{st} (x) \to A^{n} = A^{suc 1^{st} (x)}$
15	14	eliuni	$⊢ (suc 1^{st} (x) \in ω \land suc 1^{st} (x) \times \{2^{nd} (x)\} \in (A^{suc 1^{st} (x)})) \to suc 1^{st} (x) \times \{2^{nd} (x)\} \in ⋃_{n \in ω} (A^{n})$
16	6 13 15	syl2an2	$⊢ (A \in V \land x \in (ω \times A)) \to suc 1^{st} (x) \times \{2^{nd} (x)\} \in ⋃_{n \in ω} (A^{n})$
17	16	ex	$⊢ A \in V \to (x \in (ω \times A) \to suc 1^{st} (x) \times \{2^{nd} (x)\} \in ⋃_{n \in ω} (A^{n}))$
18		nsuceq0	$⊢ suc 1^{st} (x) \neq \emptyset$
19		fvex	$⊢ 2^{nd} (x) \in V$
20	19	snnz	$⊢ \{2^{nd} (x)\} \neq \emptyset$
21		xp11	$⊢ (suc 1^{st} (x) \neq \emptyset \land \{2^{nd} (x)\} \neq \emptyset) \to (suc 1^{st} (x) \times \{2^{nd} (x)\} = suc 1^{st} (y) \times \{2^{nd} (y)\} \leftrightarrow (suc 1^{st} (x) = suc 1^{st} (y) \land \{2^{nd} (x)\} = \{2^{nd} (y)\}))$
22	18 20 21	mp2an	$⊢ suc 1^{st} (x) \times \{2^{nd} (x)\} = suc 1^{st} (y) \times \{2^{nd} (y)\} \leftrightarrow (suc 1^{st} (x) = suc 1^{st} (y) \land \{2^{nd} (x)\} = \{2^{nd} (y)\})$
23		xp1st	$⊢ y \in (ω \times A) \to 1^{st} (y) \in ω$
24		peano4	$⊢ (1^{st} (x) \in ω \land 1^{st} (y) \in ω) \to (suc 1^{st} (x) = suc 1^{st} (y) \leftrightarrow 1^{st} (x) = 1^{st} (y))$
25	4 23 24	syl2an	$⊢ (x \in (ω \times A) \land y \in (ω \times A)) \to (suc 1^{st} (x) = suc 1^{st} (y) \leftrightarrow 1^{st} (x) = 1^{st} (y))$
26		sneqbg	$⊢ 2^{nd} (x) \in V \to (\{2^{nd} (x)\} = \{2^{nd} (y)\} \leftrightarrow 2^{nd} (x) = 2^{nd} (y))$
27	19 26	mp1i	$⊢ (x \in (ω \times A) \land y \in (ω \times A)) \to (\{2^{nd} (x)\} = \{2^{nd} (y)\} \leftrightarrow 2^{nd} (x) = 2^{nd} (y))$
28	25 27	anbi12d	$⊢ (x \in (ω \times A) \land y \in (ω \times A)) \to ((suc 1^{st} (x) = suc 1^{st} (y) \land \{2^{nd} (x)\} = \{2^{nd} (y)\}) \leftrightarrow (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y)))$
29	22 28	bitrid	$⊢ (x \in (ω \times A) \land y \in (ω \times A)) \to (suc 1^{st} (x) \times \{2^{nd} (x)\} = suc 1^{st} (y) \times \{2^{nd} (y)\} \leftrightarrow (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y)))$
30		xpopth	$⊢ (x \in (ω \times A) \land y \in (ω \times A)) \to ((1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y)) \leftrightarrow x = y)$
31	29 30	bitrd	$⊢ (x \in (ω \times A) \land y \in (ω \times A)) \to (suc 1^{st} (x) \times \{2^{nd} (x)\} = suc 1^{st} (y) \times \{2^{nd} (y)\} \leftrightarrow x = y)$
32	31	a1i	$⊢ A \in V \to ((x \in (ω \times A) \land y \in (ω \times A)) \to (suc 1^{st} (x) \times \{2^{nd} (x)\} = suc 1^{st} (y) \times \{2^{nd} (y)\} \leftrightarrow x = y))$
33	17 32	dom2d	$⊢ A \in V \to (⋃_{n \in ω} (A^{n}) \in V \to (ω \times A) ≼ ⋃_{n \in ω} (A^{n}))$
34	3 33	mpi	$⊢ A \in V \to (ω \times A) ≼ ⋃_{n \in ω} (A^{n})$

Metamath Proof Explorer

Theorem fseqdom

Proof