Theorem tfrlemibxssdm 5882

Description: The union of B is defined on all ordinals. Lemma for tfrlemi1 5887. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)

Hypotheses

Ref	Expression
tfrlemisucfn.1	|- A = {f | E.x e. On (f Fn x /\ A.y e. x (f ` y) = ( F ` (f |` y))) }
tfrlemisucfn.2	|- (ph -> A.x( Fun F /\ ( F ` x) e. _V))
tfrlemi1.3	|- B = { h | E.z e. x E.g(g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. })) }
tfrlemi1.4	|- (ph -> x e. On)
tfrlemi1.5	|- (ph -> A.z e. x E.g(g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))))

Assertion

Ref	Expression
tfrlemibxssdm	|- (ph -> x C_ dom U.B)

Distinct variable groups:   f,g, h,w,x,y,z,A   f, F,g, h,w,x,y,z   ph,w,y   w,B,f,g, h,z   ph,g, h,z

Allowed substitution hints:   ph(x,f)   B(x,y)

Proof of Theorem tfrlemibxssdm

Step	Hyp	Ref	Expression
1		tfrlemi1.5	. . 3 |- (ph -> A.z e. x E.g(g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))))
2		tfrlemi1.4	. . . 4 |- (ph -> x e. On)
3		tfrlemisucfn.2	. . . . . . . . . . . 12 |- (ph -> A.x( Fun F /\ ( F ` x) e. _V))
4	3	tfrlem3-2d 5869	. . . . . . . . . . 11 |- (ph -> ( Fun F /\ ( F ` g) e. _V))
5	4	simprd 107	. . . . . . . . . 10 |- (ph -> ( F ` g) e. _V)
6	5	3ad2ant1 924	. . . . . . . . 9 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> ( F ` g) e. _V)
7		vex 2554	. . . . . . . . . . . . 13 |- z e. _V
8		opexg 3955	. . . . . . . . . . . . 13 |- ((z e. _V /\ ( F ` g) e. _V) -> <.z , ( F ` g) >. e. _V)
9	7, 5, 8	sylancr 393	. . . . . . . . . . . 12 |- (ph -> <.z , ( F ` g) >. e. _V)
10		snidg 3392	. . . . . . . . . . . 12 |- ( <.z , ( F ` g) >. e. _V -> <.z , ( F ` g) >. e. { <.z , ( F ` g) >. })
11		elun2 3105	. . . . . . . . . . . 12 |- ( <.z , ( F ` g) >. e. { <.z , ( F ` g) >. } -> <.z , ( F ` g) >. e. (g u. { <.z , ( F ` g) >. }))
12	9, 10, 11	3syl 17	. . . . . . . . . . 11 |- (ph -> <.z , ( F ` g) >. e. (g u. { <.z , ( F ` g) >. }))
13	12	3ad2ant1 924	. . . . . . . . . 10 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> <.z , ( F ` g) >. e. (g u. { <.z , ( F ` g) >. }))
14		simp2r 930	. . . . . . . . . . . 12 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> z e. x)
15		simp3l 931	. . . . . . . . . . . 12 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> g Fn z)
16		onelon 4087	. . . . . . . . . . . . . . 15 |- ((x e. On /\ z e. x) -> z e. On)
17		rspe 2364	. . . . . . . . . . . . . . 15 |- ((z e. On /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> E.z e. On (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))))
18	16, 17	sylan 267	. . . . . . . . . . . . . 14 |- (((x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> E.z e. On (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))))
19		tfrlemisucfn.1	. . . . . . . . . . . . . . 15 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f ` y) = ( F ` (f |` y))) }
20		vex 2554	. . . . . . . . . . . . . . 15 |- g e. _V
21	19, 20	tfrlem3a 5866	. . . . . . . . . . . . . 14 |- (g e. A <-> E.z e. On (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))))
22	18, 21	sylibr 137	. . . . . . . . . . . . 13 |- (((x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> g e. A)
23	22	3adant1 921	. . . . . . . . . . . 12 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> g e. A)
24	14, 15, 23	3jca 1083	. . . . . . . . . . 11 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> (z e. x /\ g Fn z /\ g e. A))
25		snexg 3927	. . . . . . . . . . . . . 14 |- ( <.z , ( F ` g) >. e. _V -> { <.z , ( F ` g) >. } e. _V)
26		unexg 4144	. . . . . . . . . . . . . . 15 |- ((g e. _V /\ { <.z , ( F ` g) >. } e. _V) -> (g u. { <.z , ( F ` g) >. }) e. _V)
27	20, 26	mpan 400	. . . . . . . . . . . . . 14 |- ( { <.z , ( F ` g) >. } e. _V -> (g u. { <.z , ( F ` g) >. }) e. _V)
28	9, 25, 27	3syl 17	. . . . . . . . . . . . 13 |- (ph -> (g u. { <.z , ( F ` g) >. }) e. _V)
29		isset 2555	. . . . . . . . . . . . 13 |- ((g u. { <.z , ( F ` g) >. }) e. _V <-> E. h h = (g u. { <.z , ( F ` g) >. }))
30	28, 29	sylib 127	. . . . . . . . . . . 12 |- (ph -> E. h h = (g u. { <.z , ( F ` g) >. }))
31	30	3ad2ant1 924	. . . . . . . . . . 11 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> E. h h = (g u. { <.z , ( F ` g) >. }))
32		simpr3 911	. . . . . . . . . . . . . . 15 |- ((z e. x /\ (g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. }))) -> h = (g u. { <.z , ( F ` g) >. }))
33		19.8a 1479	. . . . . . . . . . . . . . . 16 |- ((g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. })) -> E.g(g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. })))
34		rspe 2364	. . . . . . . . . . . . . . . . 17 |- ((z e. x /\ E.g(g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. }))) -> E.z e. x E.g(g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. })))
35		tfrlemi1.3	. . . . . . . . . . . . . . . . . 18 |- B = { h | E.z e. x E.g(g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. })) }
36	35	abeq2i 2145	. . . . . . . . . . . . . . . . 17 |- ( h e. B <-> E.z e. x E.g(g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. })))
37	34, 36	sylibr 137	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ E.g(g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. }))) -> h e. B)
38	33, 37	sylan2 270	. . . . . . . . . . . . . . 15 |- ((z e. x /\ (g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. }))) -> h e. B)
39	32, 38	eqeltrrd 2112	. . . . . . . . . . . . . 14 |- ((z e. x /\ (g Fn z /\ g e. A /\ h = (g u. { <.z , ( F ` g) >. }))) -> (g u. { <.z , ( F ` g) >. }) e. B)
40	39	3exp2 1121	. . . . . . . . . . . . 13 |- (z e. x -> (g Fn z -> (g e. A -> ( h = (g u. { <.z , ( F ` g) >. }) -> (g u. { <.z , ( F ` g) >. }) e. B))))
41	40	3imp 1097	. . . . . . . . . . . 12 |- ((z e. x /\ g Fn z /\ g e. A) -> ( h = (g u. { <.z , ( F ` g) >. }) -> (g u. { <.z , ( F ` g) >. }) e. B))
42	41	exlimdv 1697	. . . . . . . . . . 11 |- ((z e. x /\ g Fn z /\ g e. A) -> (E. h h = (g u. { <.z , ( F ` g) >. }) -> (g u. { <.z , ( F ` g) >. }) e. B))
43	24, 31, 42	sylc 56	. . . . . . . . . 10 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> (g u. { <.z , ( F ` g) >. }) e. B)
44		elunii 3576	. . . . . . . . . 10 |- (( <.z , ( F ` g) >. e. (g u. { <.z , ( F ` g) >. }) /\ (g u. { <.z , ( F ` g) >. }) e. B) -> <.z , ( F ` g) >. e. U.B)
45	13, 43, 44	syl2anc 391	. . . . . . . . 9 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> <.z , ( F ` g) >. e. U.B)
46		opeq2 3541	. . . . . . . . . . . 12 |- (w = ( F ` g) -> <.z , w >. = <.z , ( F ` g) >.)
47	46	eleq1d 2103	. . . . . . . . . . 11 |- (w = ( F ` g) -> ( <.z , w >. e. U.B <-> <.z , ( F ` g) >. e. U.B))
48	47	spcegv 2635	. . . . . . . . . 10 |- (( F ` g) e. _V -> ( <.z , ( F ` g) >. e. U.B -> E.w <.z , w >. e. U.B))
49	7	eldm2 4476	. . . . . . . . . 10 |- (z e. dom U.B <-> E.w <.z , w >. e. U.B)
50	48, 49	syl6ibr 151	. . . . . . . . 9 |- (( F ` g) e. _V -> ( <.z , ( F ` g) >. e. U.B -> z e. dom U.B))
51	6, 45, 50	sylc 56	. . . . . . . 8 |- ((ph /\ (x e. On /\ z e. x) /\ (g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w)))) -> z e. dom U.B)
52	51	3expia 1105	. . . . . . 7 |- ((ph /\ (x e. On /\ z e. x)) -> ((g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))) -> z e. dom U.B))
53	52	exlimdv 1697	. . . . . 6 |- ((ph /\ (x e. On /\ z e. x)) -> (E.g(g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))) -> z e. dom U.B))
54	53	anassrs 380	. . . . 5 |- (((ph /\ x e. On) /\ z e. x) -> (E.g(g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))) -> z e. dom U.B))
55	54	ralimdva 2381	. . . 4 |- ((ph /\ x e. On) -> (A.z e. x E.g(g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))) -> A.z e. x z e. dom U.B))
56	2, 55	mpdan 398	. . 3 |- (ph -> (A.z e. x E.g(g Fn z /\ A.w e. z (g ` w) = ( F ` (g |` w))) -> A.z e. x z e. dom U.B))
57	1, 56	mpd 13	. 2 |- (ph -> A.z e. x z e. dom U.B)
58		dfss3 2929	. 2 |- (x C_ dom U.B <-> A.z e. x z e. dom U.B)
59	57, 58	sylibr 137	1 |- (ph -> x C_ dom U.B)

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 884  A.wal 1240   = wceq 1242  E.wex 1378   e. wcel 1390   {cab 2023  A.wral 2300  E.wrex 2301   _Vcvv 2551   u. cun 2909   C_ wss 2911   {csn 3367   <.cop 3370   U.cuni 3571   Oncon0 4066   dom cdm 4288   |` cres 4290   Fun wfun 4839   Fn wfn 4840   ` cfv 4845

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-tr 3846  df-iord 4069  df-on 4071  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853

This theorem is referenced by:  tfrlemibfn  5883