Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 onovuni.1 ⊢ ( Lim 𝑦 → ( 𝐴 𝐹 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐴 𝐹 𝑥 ) )
2 onovuni.2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐴 𝐹 𝑥 ) ⊆ ( 𝐴 𝐹 𝑦 ) )
3 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐴 𝐹 𝑧 ) = ( 𝐴 𝐹 𝑦 ) )
4 eqid ⊢ ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) = ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) )
5 ovex ⊢ ( 𝐴 𝐹 𝑦 ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑦 ∈ V → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑦 ) = ( 𝐴 𝐹 𝑦 ) )
7 6 elv ⊢ ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑦 ) = ( 𝐴 𝐹 𝑦 )
8 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐴 𝐹 𝑧 ) = ( 𝐴 𝐹 𝑥 ) )
9 ovex ⊢ ( 𝐴 𝐹 𝑥 ) ∈ V
10 8 4 9 fvmpt ⊢ ( 𝑥 ∈ V → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) = ( 𝐴 𝐹 𝑥 ) )
11 10 elv ⊢ ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) = ( 𝐴 𝐹 𝑥 )
12 11 a1i ⊢ ( 𝑥 ∈ 𝑦 → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) = ( 𝐴 𝐹 𝑥 ) )
13 12 iuneq2i ⊢ ∪ 𝑥 ∈ 𝑦 ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐴 𝐹 𝑥 )
14 1 7 13 3eqtr4g ⊢ ( Lim 𝑦 → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) )
15 2 11 7 3sstr4g ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) ⊆ ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑦 ) )
16 14 15 onfununi ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) )
17 uniexg ⊢ ( 𝑆 ∈ 𝑇 → ∪ 𝑆 ∈ V )
18 oveq2 ⊢ ( 𝑧 = ∪ 𝑆 → ( 𝐴 𝐹 𝑧 ) = ( 𝐴 𝐹 ∪ 𝑆 ) )
19 ovex ⊢ ( 𝐴 𝐹 ∪ 𝑆 ) ∈ V
20 18 4 19 fvmpt ⊢ ( ∪ 𝑆 ∈ V → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ ∪ 𝑆 ) = ( 𝐴 𝐹 ∪ 𝑆 ) )
21 17 20 syl ⊢ ( 𝑆 ∈ 𝑇 → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ ∪ 𝑆 ) = ( 𝐴 𝐹 ∪ 𝑆 ) )
22 21 3ad2ant1 ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ ∪ 𝑆 ) = ( 𝐴 𝐹 ∪ 𝑆 ) )
23 11 a1i ⊢ ( 𝑥 ∈ 𝑆 → ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) = ( 𝐴 𝐹 𝑥 ) )
24 23 iuneq2i ⊢ ∪ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝑆 ( 𝐴 𝐹 𝑥 )
25 24 a1i ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ∪ 𝑥 ∈ 𝑆 ( ( 𝑧 ∈ V ↦ ( 𝐴 𝐹 𝑧 ) ) ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝑆 ( 𝐴 𝐹 𝑥 ) )
26 16 22 25 3eqtr3d ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( 𝐴 𝐹 ∪ 𝑆 ) = ∪ 𝑥 ∈ 𝑆 ( 𝐴 𝐹 𝑥 ) )