This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsvallem

Description: Lemma for prdsval . (Contributed by Stefan O'Rear, 3-Jan-2015) Extracted from the former proof of prdsval , dependency on df-hom removed. (Revised by AV, 13-Oct-2024)

Ref Expression
Assertion prdsvallem ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑣 ∈ V
2 ovex ⊢ ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) ∈ V
3 2 pwex ⊢ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) ∈ V
4 ovssunirn ⊢ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) )
5 homid ⊢ Hom = Slot ( Hom ‘ ndx )
6 5 strfvss ⊢ ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ( 𝑟 ‘ 𝑥 )
7 fvssunirn ⊢ ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran 𝑟
8 rnss ⊢ ( ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran 𝑟 → ran ( 𝑟 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑟 )
9 uniss ⊢ ( ran ( 𝑟 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑟 → ∪ ran ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑟 )
10 7 8 9 mp2b ⊢ ∪ ran ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑟
11 6 10 sstri ⊢ ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
12 rnss ⊢ ( ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟 → ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ran ∪ ran ∪ ran 𝑟 )
13 uniss ⊢ ( ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ran ∪ ran ∪ ran 𝑟 → ∪ ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟 )
14 11 12 13 mp2b ⊢ ∪ ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
15 4 14 sstri ⊢ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
16 15 rgenw ⊢ ∀ 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
17 ss2ixp ⊢ ( ∀ 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟 → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ dom 𝑟 ∪ ran ∪ ran ∪ ran 𝑟 )
18 16 17 ax-mp ⊢ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ dom 𝑟 ∪ ran ∪ ran ∪ ran 𝑟
19 vex ⊢ 𝑟 ∈ V
20 19 dmex ⊢ dom 𝑟 ∈ V
21 19 rnex ⊢ ran 𝑟 ∈ V
22 21 uniex ⊢ ∪ ran 𝑟 ∈ V
23 22 rnex ⊢ ran ∪ ran 𝑟 ∈ V
24 23 uniex ⊢ ∪ ran ∪ ran 𝑟 ∈ V
25 24 rnex ⊢ ran ∪ ran ∪ ran 𝑟 ∈ V
26 25 uniex ⊢ ∪ ran ∪ ran ∪ ran 𝑟 ∈ V
27 20 26 ixpconst ⊢ X 𝑥 ∈ dom 𝑟 ∪ ran ∪ ran ∪ ran 𝑟 = ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
28 18 27 sseqtri ⊢ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
29 2 28 elpwi2 ⊢ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
30 29 rgen2w ⊢ ∀ 𝑓 ∈ 𝑣 ∀ 𝑔 ∈ 𝑣 X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
31 1 1 3 30 mpoexw ⊢ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V