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 y A F y = x y A F x
onovuni.2 x On y On x y A F x A F y
Assertion onovuni S T S On S A F S = x S A F x

Proof

Step Hyp Ref Expression
1 onovuni.1 Lim y A F y = x y A F x
2 onovuni.2 x On y On x y A F x A F y
3 oveq2 z = y A F z = A F y
4 eqid z V A F z = z V A F z
5 ovex A F y V
6 3 4 5 fvmpt y V z V A F z y = A F y
7 6 elv z V A F z y = A F y
8 oveq2 z = x A F z = A F x
9 ovex A F x V
10 8 4 9 fvmpt x V z V A F z x = A F x
11 10 elv z V A F z x = A F x
12 11 a1i x y z V A F z x = A F x
13 12 iuneq2i x y z V A F z x = x y A F x
14 1 7 13 3eqtr4g Lim y z V A F z y = x y z V A F z x
15 2 11 7 3sstr4g x On y On x y z V A F z x z V A F z y
16 14 15 onfununi S T S On S z V A F z S = x S z V A F z x
17 uniexg S T S V
18 oveq2 z = S A F z = A F S
19 ovex A F S V
20 18 4 19 fvmpt S V z V A F z S = A F S
21 17 20 syl S T z V A F z S = A F S
22 21 3ad2ant1 S T S On S z V A F z S = A F S
23 11 a1i x S z V A F z x = A F x
24 23 iuneq2i x S z V A F z x = x S A F x
25 24 a1i S T S On S x S z V A F z x = x S A F x
26 16 22 25 3eqtr3d S T S On S A F S = x S A F x