onovuni

Description: A variant of onfununi for operations. (Contributed by Eric Schmidt, 26-May-2009) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	onovuni.1	$⊢ Lim y \to A F y = ⋃_{x \in y} (A F x)$
	onovuni.2	$⊢ (x \in On \land y \in On \land x \subseteq y) \to A F x \subseteq A F y$
Assertion	onovuni	$⊢ (S \in T \land S \subseteq On \land S \neq \emptyset) \to A F ⋃ S = ⋃_{x \in S} (A F x)$

Proof

Step	Hyp	Ref	Expression
1		onovuni.1	$⊢ Lim y \to A F y = ⋃_{x \in y} (A F x)$
2		onovuni.2	$⊢ (x \in On \land y \in On \land x \subseteq y) \to A F x \subseteq A F y$
3		oveq2	$⊢ z = y \to A F z = A F y$
4		eqid	$⊢ (z \in V ⟼ A F z) = (z \in V ⟼ A F z)$
5		ovex	$⊢ A F y \in V$
6	3 4 5	fvmpt	$⊢ y \in V \to (z \in V ⟼ A F z) (y) = A F y$
7	6	elv	$⊢ (z \in V ⟼ A F z) (y) = A F y$
8		oveq2	$⊢ z = x \to A F z = A F x$
9		ovex	$⊢ A F x \in V$
10	8 4 9	fvmpt	$⊢ x \in V \to (z \in V ⟼ A F z) (x) = A F x$
11	10	elv	$⊢ (z \in V ⟼ A F z) (x) = A F x$
12	11	a1i	$⊢ x \in y \to (z \in V ⟼ A F z) (x) = A F x$
13	12	iuneq2i	$⊢ ⋃_{x \in y} (z \in V ⟼ A F z) (x) = ⋃_{x \in y} (A F x)$
14	1 7 13	3eqtr4g	$⊢ Lim y \to (z \in V ⟼ A F z) (y) = ⋃_{x \in y} (z \in V ⟼ A F z) (x)$
15	2 11 7	3sstr4g	$⊢ (x \in On \land y \in On \land x \subseteq y) \to (z \in V ⟼ A F z) (x) \subseteq (z \in V ⟼ A F z) (y)$
16	14 15	onfununi	$⊢ (S \in T \land S \subseteq On \land S \neq \emptyset) \to (z \in V ⟼ A F z) (⋃ S) = ⋃_{x \in S} (z \in V ⟼ A F z) (x)$
17		uniexg	$⊢ S \in T \to ⋃ S \in V$
18		oveq2	$⊢ z = ⋃ S \to A F z = A F ⋃ S$
19		ovex	$⊢ A F ⋃ S \in V$
20	18 4 19	fvmpt	$⊢ ⋃ S \in V \to (z \in V ⟼ A F z) (⋃ S) = A F ⋃ S$
21	17 20	syl	$⊢ S \in T \to (z \in V ⟼ A F z) (⋃ S) = A F ⋃ S$
22	21	3ad2ant1	$⊢ (S \in T \land S \subseteq On \land S \neq \emptyset) \to (z \in V ⟼ A F z) (⋃ S) = A F ⋃ S$
23	11	a1i	$⊢ x \in S \to (z \in V ⟼ A F z) (x) = A F x$
24	23	iuneq2i	$⊢ ⋃_{x \in S} (z \in V ⟼ A F z) (x) = ⋃_{x \in S} (A F x)$
25	24	a1i	$⊢ (S \in T \land S \subseteq On \land S \neq \emptyset) \to ⋃_{x \in S} (z \in V ⟼ A F z) (x) = ⋃_{x \in S} (A F x)$
26	16 22 25	3eqtr3d	$⊢ (S \in T \land S \subseteq On \land S \neq \emptyset) \to A F ⋃ S = ⋃_{x \in S} (A F x)$

Metamath Proof Explorer

Theorem onovuni

Proof