Theorem prdsvallem 13506

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

Assertion

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

Distinct variable groups:   𝑥,𝑟   𝑓,𝑔,𝑟   𝑣,𝑓,𝑔

Proof of Theorem prdsvallem

Step	Hyp	Ref	Expression
1		vex 2818	. 2 ⊢ 𝑣 ∈ V
2		fnmap 6891	. . . 4 ⊢ ↑𝑚 Fn (V × V)
3		vex 2818	. . . . . . . . . 10 ⊢ 𝑟 ∈ V
4	3	rnex 5027	. . . . . . . . 9 ⊢ ran 𝑟 ∈ V
5	4	uniex 4560	. . . . . . . 8 ⊢ ∪ ran 𝑟 ∈ V
6	5	rnex 5027	. . . . . . 7 ⊢ ran ∪ ran 𝑟 ∈ V
7	6	uniex 4560	. . . . . 6 ⊢ ∪ ran ∪ ran 𝑟 ∈ V
8	7	rnex 5027	. . . . 5 ⊢ ran ∪ ran ∪ ran 𝑟 ∈ V
9	8	uniex 4560	. . . 4 ⊢ ∪ ran ∪ ran ∪ ran 𝑟 ∈ V
10	3	dmex 5026	. . . 4 ⊢ dom 𝑟 ∈ V
11		fnovex 6085	. . . 4 ⊢ (( ↑𝑚 Fn (V × V) ∧ ∪ ran ∪ ran ∪ ran 𝑟 ∈ V ∧ dom 𝑟 ∈ V) → (∪ ran ∪ ran ∪ ran 𝑟 ↑𝑚 dom 𝑟) ∈ V)
12	2, 9, 10, 11	mp3an 1374	. . 3 ⊢ (∪ ran ∪ ran ∪ ran 𝑟 ↑𝑚 dom 𝑟) ∈ V
13	12	pwex 4298	. 2 ⊢ 𝒫 (∪ ran ∪ ran ∪ ran 𝑟 ↑𝑚 dom 𝑟) ∈ V
14		vex 2818	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
15		vex 2818	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
16	14, 15	fvex 5692	. . . . . . . . 9 ⊢ (𝑓‘𝑥) ∈ V
17		vex 2818	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
18	17, 15	fvex 5692	. . . . . . . . 9 ⊢ (𝑔‘𝑥) ∈ V
19		ovssunirng 6087	. . . . . . . . 9 ⊢ (((𝑓‘𝑥) ∈ V ∧ (𝑔‘𝑥) ∈ V) → ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran (Hom ‘(𝑟‘𝑥)))
20	16, 18, 19	mp2an 426	. . . . . . . 8 ⊢ ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran (Hom ‘(𝑟‘𝑥))
21		homid 13468	. . . . . . . . . . . 12 ⊢ Hom = Slot (Hom ‘ndx)
22	3, 15	fvex 5692	. . . . . . . . . . . . 13 ⊢ (𝑟‘𝑥) ∈ V
23	22	a1i 9	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑟‘𝑥) ∈ V)
24		homslid 13469	. . . . . . . . . . . . . 14 ⊢ (Hom = Slot (Hom ‘ndx) ∧ (Hom ‘ndx) ∈ ℕ)
25	24	simpri 113	. . . . . . . . . . . . 13 ⊢ (Hom ‘ndx) ∈ ℕ
26	25	a1i 9	. . . . . . . . . . . 12 ⊢ (⊤ → (Hom ‘ndx) ∈ ℕ)
27	21, 23, 26	strfvssn 13255	. . . . . . . . . . 11 ⊢ (⊤ → (Hom ‘(𝑟‘𝑥)) ⊆ ∪ ran (𝑟‘𝑥))
28	27	mptru 1407	. . . . . . . . . 10 ⊢ (Hom ‘(𝑟‘𝑥)) ⊆ ∪ ran (𝑟‘𝑥)
29		fvssunirng 5687	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ V → (𝑟‘𝑥) ⊆ ∪ ran 𝑟)
30	29	elv 2819	. . . . . . . . . . 11 ⊢ (𝑟‘𝑥) ⊆ ∪ ran 𝑟
31		rnss 4989	. . . . . . . . . . 11 ⊢ ((𝑟‘𝑥) ⊆ ∪ ran 𝑟 → ran (𝑟‘𝑥) ⊆ ran ∪ ran 𝑟)
32		uniss 3937	. . . . . . . . . . 11 ⊢ (ran (𝑟‘𝑥) ⊆ ran ∪ ran 𝑟 → ∪ ran (𝑟‘𝑥) ⊆ ∪ ran ∪ ran 𝑟)
33	30, 31, 32	mp2b 8	. . . . . . . . . 10 ⊢ ∪ ran (𝑟‘𝑥) ⊆ ∪ ran ∪ ran 𝑟
34	28, 33	sstri 3249	. . . . . . . . 9 ⊢ (Hom ‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
35		rnss 4989	. . . . . . . . 9 ⊢ ((Hom ‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟 → ran (Hom ‘(𝑟‘𝑥)) ⊆ ran ∪ ran ∪ ran 𝑟)
36		uniss 3937	. . . . . . . . 9 ⊢ (ran (Hom ‘(𝑟‘𝑥)) ⊆ ran ∪ ran ∪ ran 𝑟 → ∪ ran (Hom ‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran ∪ ran 𝑟)
37	34, 35, 36	mp2b 8	. . . . . . . 8 ⊢ ∪ ran (Hom ‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
38	20, 37	sstri 3249	. . . . . . 7 ⊢ ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
39	38	rgenw 2599	. . . . . 6 ⊢ ∀𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
40		ss2ixp 6948	. . . . . 6 ⊢ (∀𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran ∪ ran ∪ ran 𝑟 → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ X𝑥 ∈ dom 𝑟∪ ran ∪ ran ∪ ran 𝑟)
41	39, 40	ax-mp 5	. . . . 5 ⊢ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ X𝑥 ∈ dom 𝑟∪ ran ∪ ran ∪ ran 𝑟
42	10, 9	ixpconst 6945	. . . . 5 ⊢ X𝑥 ∈ dom 𝑟∪ ran ∪ ran ∪ ran 𝑟 = (∪ ran ∪ ran ∪ ran 𝑟 ↑𝑚 dom 𝑟)
43	41, 42	sseqtri 3274	. . . 4 ⊢ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ⊆ (∪ ran ∪ ran ∪ ran 𝑟 ↑𝑚 dom 𝑟)
44	12, 43	elpwi2 4272	. . 3 ⊢ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ∈ 𝒫 (∪ ran ∪ ran ∪ ran 𝑟 ↑𝑚 dom 𝑟)
45	44	rgen2w 2600	. 2 ⊢ ∀𝑓 ∈ 𝑣 ∀𝑔 ∈ 𝑣 X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) ∈ 𝒫 (∪ ran ∪ ran ∪ ran 𝑟 ↑𝑚 dom 𝑟)
46	1, 1, 13, 45	mpoexw 6411	1 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V

Syntax hints:   = wceq 1398  ⊤wtru 1399   ∈ wcel 2205  ∀wral 2522  Vcvv 2815   ⊆ wss 3213  𝒫 cpw 3671  ∪ cuni 3916   × cxp 4749  dom cdm 4751  ran crn 4752   Fn wfn 5349  ‘cfv 5354  (class class class)co 6052   ∈ cmpo 6054   ↑_𝑚 cmap 6884  Xcixp 6935  ℕcn 9242  ndxcnx 13230  Slot cslot 13232  Hom chom 13322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-cnex 8223  ax-resscn 8224  ax-1cn 8225  ax-1re 8226  ax-icn 8227  ax-addcl 8228  ax-addrcl 8229  ax-mulcl 8230  ax-addcom 8232  ax-mulcom 8233  ax-addass 8234  ax-mulass 8235  ax-distr 8236  ax-i2m1 8237  ax-1rid 8239  ax-0id 8240  ax-rnegex 8241  ax-cnre 8243

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3045  df-csb 3141  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-iun 3995  df-br 4112  df-opab 4174  df-mpt 4175  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-res 4763  df-ima 4764  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-fv 5362  df-riota 6005  df-ov 6055  df-oprab 6056  df-mpo 6057  df-1st 6336  df-2nd 6337  df-map 6886  df-ixp 6936  df-sub 8451  df-inn 9243  df-2 9301  df-3 9302  df-4 9303  df-5 9304  df-6 9305  df-7 9306  df-8 9307  df-9 9308  df-n0 9502  df-dec 9716  df-ndx 13236  df-slot 13237  df-hom 13335

This theorem is referenced by:  prdsval  13507