frege131d

Description: If F is a function and A contains all elements of U and all elements before or after those elements of U in the transitive closure of F , then the image under F of A is a subclass of A . Similar to Proposition 131 of Frege1879 p. 85. Compare with frege131 . (Contributed by RP, 17-Jul-2020)

	Ref	Expression
Hypotheses	frege131d.f	$⊢ φ \to F \in V$
	frege131d.a	$⊢ φ \to A = U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
	frege131d.fun	$⊢ φ \to Fun F$
Assertion	frege131d	$⊢ φ \to F [A] \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		frege131d.f	$⊢ φ \to F \in V$
2		frege131d.a	$⊢ φ \to A = U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
3		frege131d.fun	$⊢ φ \to Fun F$
4		trclfvlb	$⊢ F \in V \to F \subseteq t+ (F)$
5		imass1	$⊢ F \subseteq t+ (F) \to F [U] \subseteq t+ (F) [U]$
6	1 4 5	3syl	$⊢ φ \to F [U] \subseteq t+ (F) [U]$
7		ssun2	$⊢ t+ (F) [U] \subseteq {t+ (F)}^{-1} [U] \cup t+ (F) [U]$
8		ssun2	$⊢ {t+ (F)}^{-1} [U] \cup t+ (F) [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
9	7 8	sstri	$⊢ t+ (F) [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
10	6 9	sstrdi	$⊢ φ \to F [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
11		trclfvdecomr	$⊢ F \in V \to t+ (F) = F \cup (t+ (F) \circ F)$
12	1 11	syl	$⊢ φ \to t+ (F) = F \cup (t+ (F) \circ F)$
13	12	cnveqd	$⊢ φ \to {t+ (F)}^{-1} = {(F \cup (t+ (F) \circ F))}^{-1}$
14		cnvun	$⊢ {(F \cup (t+ (F) \circ F))}^{-1} = F^{-1} \cup {(t+ (F) \circ F)}^{-1}$
15		cnvco	$⊢ {(t+ (F) \circ F)}^{-1} = F^{-1} \circ {t+ (F)}^{-1}$
16	15	uneq2i	$⊢ F^{-1} \cup {(t+ (F) \circ F)}^{-1} = F^{-1} \cup (F^{-1} \circ {t+ (F)}^{-1})$
17	14 16	eqtri	$⊢ {(F \cup (t+ (F) \circ F))}^{-1} = F^{-1} \cup (F^{-1} \circ {t+ (F)}^{-1})$
18	13 17	eqtrdi	$⊢ φ \to {t+ (F)}^{-1} = F^{-1} \cup (F^{-1} \circ {t+ (F)}^{-1})$
19	18	coeq2d	$⊢ φ \to F \circ {t+ (F)}^{-1} = F \circ (F^{-1} \cup (F^{-1} \circ {t+ (F)}^{-1}))$
20		coundi	$⊢ F \circ (F^{-1} \cup (F^{-1} \circ {t+ (F)}^{-1})) = (F \circ F^{-1}) \cup (F \circ (F^{-1} \circ {t+ (F)}^{-1}))$
21		funcocnv2	$⊢ Fun F \to F \circ F^{-1} = {I ↾}_{ran F}$
22	3 21	syl	$⊢ φ \to F \circ F^{-1} = {I ↾}_{ran F}$
23		coass	$⊢ (F \circ F^{-1}) \circ {t+ (F)}^{-1} = F \circ (F^{-1} \circ {t+ (F)}^{-1})$
24	23	eqcomi	$⊢ F \circ (F^{-1} \circ {t+ (F)}^{-1}) = (F \circ F^{-1}) \circ {t+ (F)}^{-1}$
25	22	coeq1d	$⊢ φ \to (F \circ F^{-1}) \circ {t+ (F)}^{-1} = ({I ↾}_{ran F}) \circ {t+ (F)}^{-1}$
26	24 25	syl5eq	$⊢ φ \to F \circ (F^{-1} \circ {t+ (F)}^{-1}) = ({I ↾}_{ran F}) \circ {t+ (F)}^{-1}$
27	22 26	uneq12d	$⊢ φ \to (F \circ F^{-1}) \cup (F \circ (F^{-1} \circ {t+ (F)}^{-1})) = ({I ↾}_{ran F}) \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1})$
28	20 27	syl5eq	$⊢ φ \to F \circ (F^{-1} \cup (F^{-1} \circ {t+ (F)}^{-1})) = ({I ↾}_{ran F}) \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1})$
29	19 28	eqtrd	$⊢ φ \to F \circ {t+ (F)}^{-1} = ({I ↾}_{ran F}) \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1})$
30	29	imaeq1d	$⊢ φ \to (F \circ {t+ (F)}^{-1}) [U] = (({I ↾}_{ran F}) \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1})) [U]$
31		imaundir	$⊢ (({I ↾}_{ran F}) \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1})) [U] = ({I ↾}_{ran F}) [U] \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U]$
32	30 31	eqtrdi	$⊢ φ \to (F \circ {t+ (F)}^{-1}) [U] = ({I ↾}_{ran F}) [U] \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U]$
33		resss	$⊢ {I ↾}_{ran F} \subseteq I$
34		imass1	$⊢ {I ↾}_{ran F} \subseteq I \to ({I ↾}_{ran F}) [U] \subseteq I [U]$
35	33 34	ax-mp	$⊢ ({I ↾}_{ran F}) [U] \subseteq I [U]$
36		imai	$⊢ I [U] = U$
37	35 36	sseqtri	$⊢ ({I ↾}_{ran F}) [U] \subseteq U$
38		imaco	$⊢ (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U] = ({I ↾}_{ran F}) [{t+ (F)}^{-1} [U]]$
39		imass1	$⊢ {I ↾}_{ran F} \subseteq I \to ({I ↾}_{ran F}) [{t+ (F)}^{-1} [U]] \subseteq I [{t+ (F)}^{-1} [U]]$
40	33 39	ax-mp	$⊢ ({I ↾}_{ran F}) [{t+ (F)}^{-1} [U]] \subseteq I [{t+ (F)}^{-1} [U]]$
41		imai	$⊢ I [{t+ (F)}^{-1} [U]] = {t+ (F)}^{-1} [U]$
42	40 41	sseqtri	$⊢ ({I ↾}_{ran F}) [{t+ (F)}^{-1} [U]] \subseteq {t+ (F)}^{-1} [U]$
43	38 42	eqsstri	$⊢ (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U] \subseteq {t+ (F)}^{-1} [U]$
44		unss12	$⊢ (({I ↾}_{ran F}) [U] \subseteq U \land (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U] \subseteq {t+ (F)}^{-1} [U]) \to ({I ↾}_{ran F}) [U] \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U] \subseteq U \cup {t+ (F)}^{-1} [U]$
45	37 43 44	mp2an	$⊢ ({I ↾}_{ran F}) [U] \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U] \subseteq U \cup {t+ (F)}^{-1} [U]$
46		ssun1	$⊢ U \cup {t+ (F)}^{-1} [U] \subseteq (U \cup {t+ (F)}^{-1} [U]) \cup t+ (F) [U]$
47		unass	$⊢ (U \cup {t+ (F)}^{-1} [U]) \cup t+ (F) [U] = U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
48	46 47	sseqtri	$⊢ U \cup {t+ (F)}^{-1} [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
49	45 48	sstri	$⊢ ({I ↾}_{ran F}) [U] \cup (({I ↾}_{ran F}) \circ {t+ (F)}^{-1}) [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
50	32 49	eqsstrdi	$⊢ φ \to (F \circ {t+ (F)}^{-1}) [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
51		coss1	$⊢ F \subseteq t+ (F) \to F \circ t+ (F) \subseteq t+ (F) \circ t+ (F)$
52	1 4 51	3syl	$⊢ φ \to F \circ t+ (F) \subseteq t+ (F) \circ t+ (F)$
53		trclfvcotrg	$⊢ t+ (F) \circ t+ (F) \subseteq t+ (F)$
54	52 53	sstrdi	$⊢ φ \to F \circ t+ (F) \subseteq t+ (F)$
55		imass1	$⊢ F \circ t+ (F) \subseteq t+ (F) \to (F \circ t+ (F)) [U] \subseteq t+ (F) [U]$
56	54 55	syl	$⊢ φ \to (F \circ t+ (F)) [U] \subseteq t+ (F) [U]$
57	56 9	sstrdi	$⊢ φ \to (F \circ t+ (F)) [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
58	50 57	unssd	$⊢ φ \to (F \circ {t+ (F)}^{-1}) [U] \cup (F \circ t+ (F)) [U] \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
59	10 58	unssd	$⊢ φ \to F [U] \cup ((F \circ {t+ (F)}^{-1}) [U] \cup (F \circ t+ (F)) [U]) \subseteq U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])$
60	2	imaeq2d	$⊢ φ \to F [A] = F [U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])]$
61		imaundi	$⊢ F [U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])] = F [U] \cup F [{t+ (F)}^{-1} [U] \cup t+ (F) [U]]$
62		imaundi	$⊢ F [{t+ (F)}^{-1} [U] \cup t+ (F) [U]] = F [{t+ (F)}^{-1} [U]] \cup F [t+ (F) [U]]$
63		imaco	$⊢ (F \circ {t+ (F)}^{-1}) [U] = F [{t+ (F)}^{-1} [U]]$
64	63	eqcomi	$⊢ F [{t+ (F)}^{-1} [U]] = (F \circ {t+ (F)}^{-1}) [U]$
65		imaco	$⊢ (F \circ t+ (F)) [U] = F [t+ (F) [U]]$
66	65	eqcomi	$⊢ F [t+ (F) [U]] = (F \circ t+ (F)) [U]$
67	64 66	uneq12i	$⊢ F [{t+ (F)}^{-1} [U]] \cup F [t+ (F) [U]] = (F \circ {t+ (F)}^{-1}) [U] \cup (F \circ t+ (F)) [U]$
68	62 67	eqtri	$⊢ F [{t+ (F)}^{-1} [U] \cup t+ (F) [U]] = (F \circ {t+ (F)}^{-1}) [U] \cup (F \circ t+ (F)) [U]$
69	68	uneq2i	$⊢ F [U] \cup F [{t+ (F)}^{-1} [U] \cup t+ (F) [U]] = F [U] \cup ((F \circ {t+ (F)}^{-1}) [U] \cup (F \circ t+ (F)) [U])$
70	61 69	eqtri	$⊢ F [U \cup ({t+ (F)}^{-1} [U] \cup t+ (F) [U])] = F [U] \cup ((F \circ {t+ (F)}^{-1}) [U] \cup (F \circ t+ (F)) [U])$
71	60 70	eqtrdi	$⊢ φ \to F [A] = F [U] \cup ((F \circ {t+ (F)}^{-1}) [U] \cup (F \circ t+ (F)) [U])$
72	59 71 2	3sstr4d	$⊢ φ \to F [A] \subseteq A$

Metamath Proof Explorer

Theorem frege131d

Proof