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 LimyAFy=xyAFx
onovuni.2 xOnyOnxyAFxAFy
Assertion onoviun KTzKLOnKAFzKL=zKAFL

Proof

Step Hyp Ref Expression
1 onovuni.1 LimyAFy=xyAFx
2 onovuni.2 xOnyOnxyAFxAFy
3 dfiun3g zKLOnzKL=ranzKL
4 3 3ad2ant2 KTzKLOnKzKL=ranzKL
5 4 oveq2d KTzKLOnKAFzKL=AFranzKL
6 simp1 KTzKLOnKKT
7 mptexg KTzKLV
8 rnexg zKLVranzKLV
9 6 7 8 3syl KTzKLOnKranzKLV
10 simp2 KTzKLOnKzKLOn
11 eqid zKL=zKL
12 11 fmpt zKLOnzKL:KOn
13 10 12 sylib KTzKLOnKzKL:KOn
14 13 frnd KTzKLOnKranzKLOn
15 dmmptg zKLOndomzKL=K
16 15 3ad2ant2 KTzKLOnKdomzKL=K
17 simp3 KTzKLOnKK
18 16 17 eqnetrd KTzKLOnKdomzKL
19 dm0rn0 domzKL=ranzKL=
20 19 necon3bii domzKLranzKL
21 18 20 sylib KTzKLOnKranzKL
22 1 2 onovuni ranzKLVranzKLOnranzKLAFranzKL=xranzKLAFx
23 9 14 21 22 syl3anc KTzKLOnKAFranzKL=xranzKLAFx
24 oveq2 x=LAFx=AFL
25 24 eleq2d x=LwAFxwAFL
26 11 25 rexrnmptw zKLOnxranzKLwAFxzKwAFL
27 26 3ad2ant2 KTzKLOnKxranzKLwAFxzKwAFL
28 eliun wxranzKLAFxxranzKLwAFx
29 eliun wzKAFLzKwAFL
30 27 28 29 3bitr4g KTzKLOnKwxranzKLAFxwzKAFL
31 30 eqrdv KTzKLOnKxranzKLAFx=zKAFL
32 5 23 31 3eqtrd KTzKLOnKAFzKL=zKAFL