Metamath Proof Explorer

Theorem 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 𝑦 → ( 𝐴 𝐹 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐴 𝐹 𝑥 ) )
onovuni.2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐴 𝐹 𝑥 ) ⊆ ( 𝐴 𝐹 𝑦 ) )
Assertion onoviun ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ( 𝐴 𝐹 ∪ 𝑧 ∈ 𝐾 𝐿 ) = ∪ 𝑧 ∈ 𝐾 ( 𝐴 𝐹 𝐿 ) )

Proof

Step Hyp Ref Expression
1 onovuni.1 ⊢ ( Lim 𝑦 → ( 𝐴 𝐹 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐴 𝐹 𝑥 ) )
2 onovuni.2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐴 𝐹 𝑥 ) ⊆ ( 𝐴 𝐹 𝑦 ) )
3 dfiun3g ⊢ ( ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On → ∪ 𝑧 ∈ 𝐾 𝐿 = ∪ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) )
4 3 3ad2ant2 ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ∪ 𝑧 ∈ 𝐾 𝐿 = ∪ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) )
5 4 oveq2d ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ( 𝐴 𝐹 ∪ 𝑧 ∈ 𝐾 𝐿 ) = ( 𝐴 𝐹 ∪ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ) )
6 simp1 ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → 𝐾 ∈ 𝑇 )
7 mptexg ⊢ ( 𝐾 ∈ 𝑇 → ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ∈ V )
8 rnexg ⊢ ( ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ∈ V → ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ∈ V )
9 6 7 8 3syl ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ∈ V )
10 simp2 ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On )
11 eqid ⊢ ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) = ( 𝑧 ∈ 𝐾 ↦ 𝐿 )
12 11 fmpt ⊢ ( ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ↔ ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) : 𝐾 ⟶ On )
13 10 12 sylib ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) : 𝐾 ⟶ On )
14 13 frnd ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ⊆ On )
15 dmmptg ⊢ ( ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On → dom ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) = 𝐾 )
16 15 3ad2ant2 ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → dom ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) = 𝐾 )
17 simp3 ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → 𝐾 ≠ ∅ )
18 16 17 eqnetrd ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → dom ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ≠ ∅ )
19 dm0rn0 ⊢ ( dom ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) = ∅ ↔ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) = ∅ )
20 19 necon3bii ⊢ ( dom ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ≠ ∅ ↔ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ≠ ∅ )
21 18 20 sylib ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ≠ ∅ )
22 1 2 onovuni ⊢ ( ( ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ∈ V ∧ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ⊆ On ∧ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ≠ ∅ ) → ( 𝐴 𝐹 ∪ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ) = ∪ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ( 𝐴 𝐹 𝑥 ) )
23 9 14 21 22 syl3anc ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ( 𝐴 𝐹 ∪ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ) = ∪ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ( 𝐴 𝐹 𝑥 ) )
24 oveq2 ⊢ ( 𝑥 = 𝐿 → ( 𝐴 𝐹 𝑥 ) = ( 𝐴 𝐹 𝐿 ) )
25 24 eleq2d ⊢ ( 𝑥 = 𝐿 → ( 𝑤 ∈ ( 𝐴 𝐹 𝑥 ) ↔ 𝑤 ∈ ( 𝐴 𝐹 𝐿 ) ) )
26 11 25 rexrnmptw ⊢ ( ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On → ( ∃ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) 𝑤 ∈ ( 𝐴 𝐹 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐾 𝑤 ∈ ( 𝐴 𝐹 𝐿 ) ) )
27 26 3ad2ant2 ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ( ∃ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) 𝑤 ∈ ( 𝐴 𝐹 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐾 𝑤 ∈ ( 𝐴 𝐹 𝐿 ) ) )
28 eliun ⊢ ( 𝑤 ∈ ∪ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ( 𝐴 𝐹 𝑥 ) ↔ ∃ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) 𝑤 ∈ ( 𝐴 𝐹 𝑥 ) )
29 eliun ⊢ ( 𝑤 ∈ ∪ 𝑧 ∈ 𝐾 ( 𝐴 𝐹 𝐿 ) ↔ ∃ 𝑧 ∈ 𝐾 𝑤 ∈ ( 𝐴 𝐹 𝐿 ) )
30 27 28 29 3bitr4g ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ( 𝑤 ∈ ∪ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ( 𝐴 𝐹 𝑥 ) ↔ 𝑤 ∈ ∪ 𝑧 ∈ 𝐾 ( 𝐴 𝐹 𝐿 ) ) )
31 30 eqrdv ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ∪ 𝑥 ∈ ran ( 𝑧 ∈ 𝐾 ↦ 𝐿 ) ( 𝐴 𝐹 𝑥 ) = ∪ 𝑧 ∈ 𝐾 ( 𝐴 𝐹 𝐿 ) )
32 5 23 31 3eqtrd ⊢ ( ( 𝐾 ∈ 𝑇 ∧ ∀ 𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅ ) → ( 𝐴 𝐹 ∪ 𝑧 ∈ 𝐾 𝐿 ) = ∪ 𝑧 ∈ 𝐾 ( 𝐴 𝐹 𝐿 ) )