rexfiuz

Description: Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014)

		Ref	Expression
	Assertion	rexfiuz	$⊢ A \in Fin \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in A φ \leftrightarrow \forall n \in A \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$

Proof

Step	Hyp	Ref	Expression
1		raleq	$⊢ x = \emptyset \to (\forall n \in x φ \leftrightarrow \forall n \in \emptyset φ)$
2	1	rexralbidv	$⊢ x = \emptyset \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \emptyset φ)$
3		raleq	$⊢ x = \emptyset \to (\forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \forall n \in \emptyset \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
4	2 3	bibi12d	$⊢ x = \emptyset \to ((\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \emptyset φ \leftrightarrow \forall n \in \emptyset \exists j \in ℤ \forall k \in ℤ_{\geq j} φ))$
5		raleq	$⊢ x = y \to (\forall n \in x φ \leftrightarrow \forall n \in y φ)$
6	5	rexralbidv	$⊢ x = y \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ)$
7		raleq	$⊢ x = y \to (\forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \forall n \in y \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
8	6 7	bibi12d	$⊢ x = y \to ((\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \leftrightarrow \forall n \in y \exists j \in ℤ \forall k \in ℤ_{\geq j} φ))$
9		raleq	$⊢ x = y \cup \{z\} \to (\forall n \in x φ \leftrightarrow \forall n \in (y \cup \{z\}) φ)$
10	9	rexralbidv	$⊢ x = y \cup \{z\} \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in (y \cup \{z\}) φ)$
11		raleq	$⊢ x = y \cup \{z\} \to (\forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \forall n \in (y \cup \{z\}) \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
12	10 11	bibi12d	$⊢ x = y \cup \{z\} \to ((\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in (y \cup \{z\}) φ \leftrightarrow \forall n \in (y \cup \{z\}) \exists j \in ℤ \forall k \in ℤ_{\geq j} φ))$
13		raleq	$⊢ x = A \to (\forall n \in x φ \leftrightarrow \forall n \in A φ)$
14	13	rexralbidv	$⊢ x = A \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in A φ)$
15		raleq	$⊢ x = A \to (\forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \forall n \in A \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
16	14 15	bibi12d	$⊢ x = A \to ((\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in x φ \leftrightarrow \forall n \in x \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in A φ \leftrightarrow \forall n \in A \exists j \in ℤ \forall k \in ℤ_{\geq j} φ))$
17		0z	$⊢ 0 \in ℤ$
18	17	ne0ii	$⊢ ℤ \neq \emptyset$
19		ral0	$⊢ \forall n \in \emptyset φ$
20	19	rgen2w	$⊢ \forall j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \emptyset φ$
21		r19.2z	$⊢ (ℤ \neq \emptyset \land \forall j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \emptyset φ) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \emptyset φ$
22	18 20 21	mp2an	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \emptyset φ$
23		ral0	$⊢ \forall n \in \emptyset \exists j \in ℤ \forall k \in ℤ_{\geq j} φ$
24	22 23	2th	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \emptyset φ \leftrightarrow \forall n \in \emptyset \exists j \in ℤ \forall k \in ℤ_{\geq j} φ$
25		anbi1	$⊢ (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \leftrightarrow \forall n \in y \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \to ((\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \land \forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \leftrightarrow (\forall n \in y \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \land \forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ))$
26		rexanuz	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} (\forall n \in y φ \land \forall n \in \{z\} φ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \{z\} φ)$
27		ralunb	$⊢ \forall n \in (y \cup \{z\}) φ \leftrightarrow (\forall n \in y φ \land \forall n \in \{z\} φ)$
28	27	ralbii	$⊢ \forall k \in ℤ_{\geq j} \forall n \in (y \cup \{z\}) φ \leftrightarrow \forall k \in ℤ_{\geq j} (\forall n \in y φ \land \forall n \in \{z\} φ)$
29	28	rexbii	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in (y \cup \{z\}) φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (\forall n \in y φ \land \forall n \in \{z\} φ)$
30		ralsnsg	$⊢ z \in V \to (\forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \underset{˙}{[} z / n \underset{˙}{]} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
31		sbcrex	$⊢ \underset{˙}{[} z / n \underset{˙}{]} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℤ \underset{˙}{[} z / n \underset{˙}{]} \forall k \in ℤ_{\geq j} φ$
32		ralcom	$⊢ \forall k \in ℤ_{\geq j} \forall n \in \{z\} φ \leftrightarrow \forall n \in \{z\} \forall k \in ℤ_{\geq j} φ$
33		ralsnsg	$⊢ z \in V \to (\forall n \in \{z\} \forall k \in ℤ_{\geq j} φ \leftrightarrow \underset{˙}{[} z / n \underset{˙}{]} \forall k \in ℤ_{\geq j} φ)$
34	32 33	syl5bb	$⊢ z \in V \to (\forall k \in ℤ_{\geq j} \forall n \in \{z\} φ \leftrightarrow \underset{˙}{[} z / n \underset{˙}{]} \forall k \in ℤ_{\geq j} φ)$
35	34	rexbidv	$⊢ z \in V \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \{z\} φ \leftrightarrow \exists j \in ℤ \underset{˙}{[} z / n \underset{˙}{]} \forall k \in ℤ_{\geq j} φ)$
36	31 35	bitr4id	$⊢ z \in V \to (\underset{˙}{[} z / n \underset{˙}{]} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \{z\} φ)$
37	30 36	bitrd	$⊢ z \in V \to (\forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \{z\} φ)$
38	37	elv	$⊢ \forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \{z\} φ$
39	38	anbi2i	$⊢ (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \land \forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in \{z\} φ)$
40	26 29 39	3bitr4i	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in (y \cup \{z\}) φ \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \land \forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
41		ralunb	$⊢ \forall n \in (y \cup \{z\}) \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow (\forall n \in y \exists j \in ℤ \forall k \in ℤ_{\geq j} φ \land \forall n \in \{z\} \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
42	25 40 41	3bitr4g	$⊢ (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \leftrightarrow \forall n \in y \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in (y \cup \{z\}) φ \leftrightarrow \forall n \in (y \cup \{z\}) \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
43	42	a1i	$⊢ y \in Fin \to ((\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in y φ \leftrightarrow \forall n \in y \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in (y \cup \{z\}) φ \leftrightarrow \forall n \in (y \cup \{z\}) \exists j \in ℤ \forall k \in ℤ_{\geq j} φ))$
44	4 8 12 16 24 43	findcard2	$⊢ A \in Fin \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in A φ \leftrightarrow \forall n \in A \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$

Metamath Proof Explorer

Theorem rexfiuz

Proof