onoviun

Description: A variant of onovuni with indexed unions. (Contributed by Eric Schmidt, 26-May-2009) (Proof shortened by Mario Carneiro, 5-Dec-2016)

	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	onoviun	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to A F ⋃_{z \in K} L = ⋃_{z \in K} (A F L)$

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		dfiun3g	$⊢ \forall z \in K L \in On \to ⋃_{z \in K} L = ⋃ ran (z \in K ⟼ L)$
4	3	3ad2ant2	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to ⋃_{z \in K} L = ⋃ ran (z \in K ⟼ L)$
5	4	oveq2d	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to A F ⋃_{z \in K} L = A F ⋃ ran (z \in K ⟼ L)$
6		simp1	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to K \in T$
7		mptexg	$⊢ K \in T \to (z \in K ⟼ L) \in V$
8		rnexg	$⊢ (z \in K ⟼ L) \in V \to ran (z \in K ⟼ L) \in V$
9	6 7 8	3syl	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to ran (z \in K ⟼ L) \in V$
10		simp2	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to \forall z \in K L \in On$
11		eqid	$⊢ (z \in K ⟼ L) = (z \in K ⟼ L)$
12	11	fmpt	$⊢ \forall z \in K L \in On \leftrightarrow (z \in K ⟼ L) : K ⟶ On$
13	10 12	sylib	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to (z \in K ⟼ L) : K ⟶ On$
14	13	frnd	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to ran (z \in K ⟼ L) \subseteq On$
15		dmmptg	$⊢ \forall z \in K L \in On \to dom (z \in K ⟼ L) = K$
16	15	3ad2ant2	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to dom (z \in K ⟼ L) = K$
17		simp3	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to K \neq \emptyset$
18	16 17	eqnetrd	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to dom (z \in K ⟼ L) \neq \emptyset$
19		dm0rn0	$⊢ dom (z \in K ⟼ L) = \emptyset \leftrightarrow ran (z \in K ⟼ L) = \emptyset$
20	19	necon3bii	$⊢ dom (z \in K ⟼ L) \neq \emptyset \leftrightarrow ran (z \in K ⟼ L) \neq \emptyset$
21	18 20	sylib	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to ran (z \in K ⟼ L) \neq \emptyset$
22	1 2	onovuni	$⊢ (ran (z \in K ⟼ L) \in V \land ran (z \in K ⟼ L) \subseteq On \land ran (z \in K ⟼ L) \neq \emptyset) \to A F ⋃ ran (z \in K ⟼ L) = ⋃_{x \in ran (z \in K ⟼ L)} (A F x)$
23	9 14 21 22	syl3anc	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to A F ⋃ ran (z \in K ⟼ L) = ⋃_{x \in ran (z \in K ⟼ L)} (A F x)$
24		oveq2	$⊢ x = L \to A F x = A F L$
25	24	eleq2d	$⊢ x = L \to (w \in (A F x) \leftrightarrow w \in (A F L))$
26	11 25	rexrnmptw	$⊢ \forall z \in K L \in On \to (\exists x \in ran (z \in K ⟼ L) w \in (A F x) \leftrightarrow \exists z \in K w \in (A F L))$
27	26	3ad2ant2	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to (\exists x \in ran (z \in K ⟼ L) w \in (A F x) \leftrightarrow \exists z \in K w \in (A F L))$
28		eliun	$⊢ w \in ⋃_{x \in ran (z \in K ⟼ L)} (A F x) \leftrightarrow \exists x \in ran (z \in K ⟼ L) w \in (A F x)$
29		eliun	$⊢ w \in ⋃_{z \in K} (A F L) \leftrightarrow \exists z \in K w \in (A F L)$
30	27 28 29	3bitr4g	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to (w \in ⋃_{x \in ran (z \in K ⟼ L)} (A F x) \leftrightarrow w \in ⋃_{z \in K} (A F L))$
31	30	eqrdv	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to ⋃_{x \in ran (z \in K ⟼ L)} (A F x) = ⋃_{z \in K} (A F L)$
32	5 23 31	3eqtrd	$⊢ (K \in T \land \forall z \in K L \in On \land K \neq \emptyset) \to A F ⋃_{z \in K} L = ⋃_{z \in K} (A F L)$

Metamath Proof Explorer

Theorem onoviun

Proof