dfrdg4 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dfrdg4		Structured version Unicode version

Theorem dfrdg4 30667

Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Assertion**
Ref	Expression
dfrdg4	Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ

Proof of Theorem dfrdg4 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfrdg3 30394	. 2 $/\$
2		an12 804	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		df-fn 5547	. . . . . . . . . 10 $/\$
4		ancom 451	. . . . . . . . . 10 $/\$ $/\$
5		eqcom 2435	. . . . . . . . . . 11
6	5	anbi1i 699	. . . . . . . . . 10 $/\$ $/\$
7	3, 4, 6	3bitri 274	. . . . . . . . 9 $/\$
8	7	anbi1i 699	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		anass 653	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	2, 8, 9	3bitri 274	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
11	10	exbii 1712	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
12		vex 3025	. . . . . . . 8
13	12	dmex 6684	. . . . . . 7
14		eleq1 2494	. . . . . . . . 9
15		raleq 2964	. . . . . . . . 9
16	14, 15	anbi12d 715	. . . . . . . 8 $/\$ $/\$
17	16	anbi2d 708	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
18	13, 17	ceqsexv 3060	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
19	11, 18	bitri 252	. . . . 5 $/\$ $/\$ $/\$ $/\$
20		df-rex 2720	. . . . 5 $/\$ $/\$ $/\$
21		eldif 3389	. . . . . 6 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
22		elin 3592	. . . . . . . 8 Domain $/\$ Domain
23	12	elfuns 30631	. . . . . . . . 9
24	12	elima 5135	. . . . . . . . . 10 Domain Domain
25		df-rex 2720	. . . . . . . . . 10 Domain $/\$ Domain
26		ancom 451	. . . . . . . . . . . . 13 $/\$ Domain Domain $/\$
27		vex 3025	. . . . . . . . . . . . . . . 16
28	27, 12	brcnv 4979	. . . . . . . . . . . . . . 15 Domain Domain
29	12, 27	brdomain 30649	. . . . . . . . . . . . . . 15 Domain
30	28, 29	bitri 252	. . . . . . . . . . . . . 14 Domain
31	30	anbi1i 699	. . . . . . . . . . . . 13 Domain $/\$ $/\$
32	26, 31	bitri 252	. . . . . . . . . . . 12 $/\$ Domain $/\$
33	32	exbii 1712	. . . . . . . . . . 11 $/\$ Domain $/\$
34	13, 14	ceqsexv 3060	. . . . . . . . . . 11 $/\$
35	33, 34	bitri 252	. . . . . . . . . 10 $/\$ Domain
36	24, 25, 35	3bitri 274	. . . . . . . . 9 Domain
37	23, 36	anbi12i 701	. . . . . . . 8 $/\$ Domain $/\$
38	22, 37	bitri 252	. . . . . . 7 Domain $/\$
39	38	anbi1i 699	. . . . . 6 Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
40		brdif 4417	. . . . . . . . . . . . . . 15 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Apply Img FullFun Apply pprod Succ
41		vex 3025	. . . . . . . . . . . . . . . . . 18
42	12, 41	brco 4967	. . . . . . . . . . . . . . . . 17 Domain Domain $/\$
43	29	anbi1i 699	. . . . . . . . . . . . . . . . . . 19 Domain $/\$ $/\$
44	43	exbii 1712	. . . . . . . . . . . . . . . . . 18 Domain $/\$ $/\$
45		breq1 4369	. . . . . . . . . . . . . . . . . . 19
46	13, 45	ceqsexv 3060	. . . . . . . . . . . . . . . . . 18 $/\$
47	44, 46	bitri 252	. . . . . . . . . . . . . . . . 17 Domain $/\$
48	13, 41	brcnv 4979	. . . . . . . . . . . . . . . . . 18
49	13	epelc 4709	. . . . . . . . . . . . . . . . . 18
50	48, 49	bitri 252	. . . . . . . . . . . . . . . . 17
51	42, 47, 50	3bitri 274	. . . . . . . . . . . . . . . 16 Domain
52	51	anbi1i 699	. . . . . . . . . . . . . . 15 Domain $/\$ Apply Img FullFun Apply pprod Succ $/\$ Apply Img FullFun Apply pprod Succ
53	40, 52	bitri 252	. . . . . . . . . . . . . 14 Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ Apply Img FullFun Apply pprod Succ
54		onelon 5410	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56		brun 4415	. . . . . . . . . . . . . . . . . . . . . . . . 25 Img FullFun Apply pprod Succ $\/$ Img FullFun Apply pprod Succ
57		brxp 4827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58		opelxp 4826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
59	12, 58	mpbiran 926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elsn 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62		elsn 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
63	61, 62	anbi12i 701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
64	57, 63	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
65		brun 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img FullFun Apply pprod Succ Img $\/$ FullFun Apply pprod Succ
66	27	brres 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img Img $/\$
67		opex 4628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	67, 27	brco 4967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img Img $/\$
69		vex 3025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	12, 41, 69	brimg 30653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Img
71	27	brbigcup 30614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	70, 71	anbi12i 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Img $/\$ $/\$
73	72	exbii 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img $/\$ $/\$
74		imaexg 6688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75	12, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
76		unieq 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	76	eqeq1d 2430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78	75, 77	ceqsexv 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
79		eqcom 2435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
80	78, 79	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
81	68, 73, 80	3bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Img
82		opelxp 4826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
83	12, 82	mpbiran 926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84	41	ellimits 30626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	83, 84	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
86	81, 85	anbi12ci 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img $/\$ $/\$
87	66, 86	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Img $/\$
88	27	brres 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod Succ FullFun Apply pprod $/\$ Succ
89	67, 27	brco 4967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FullFun Apply pprod Apply pprod $/\$ FullFun
90		vex 3025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
91	67, 90	brco 4967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Apply pprod pprod $/\$ Apply
92	12, 41, 69	brpprod3a 30602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 pprod $/\$ $/\$
93		3anrot 987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
94	90	ideq 4949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
95		equcom 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
96	94, 95	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
97		vex 3025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
98	97	brbigcup 30614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
99		eqcom 2435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
100	98, 99	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		biid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
102	96, 100, 101	3anbi123i 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
103	93, 102	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
104	103	2exbii 1713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
105	41	uniex 6545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
106		opeq1 4130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107	106	eqeq2d 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
108		opeq2 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
109	108	eqeq2d 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
110	12, 105, 107, 109	ceqsex2v 3062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
111	92, 104, 110	3bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 pprod
112	111	anbi1i 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 pprod $/\$ Apply $/\$ Apply
113	112	exbii 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 pprod $/\$ Apply $/\$ Apply
114		opex 4628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
115		breq1 4369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Apply Apply
116	114, 115	ceqsexv 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Apply Apply
117	12, 105, 90	brapply 30654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Apply
118	116, 117	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Apply
119	91, 113, 118	3bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Apply pprod
120	90, 27	brfullfun 30664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 FullFun
121	119, 120	anbi12i 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Apply pprod $/\$ FullFun $/\$
122	121	exbii 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Apply pprod $/\$ FullFun $/\$
123		fvex 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
124		fveq2 5825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
125	124	eqeq2d 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
126	123, 125	ceqsexv 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
127	89, 122, 126	3bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FullFun Apply pprod
128		opelxp 4826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ $/\$ Succ
129	12, 128	mpbiran 926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
130	41	elrn 5037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
131	69, 41	brsuccf 30657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ
132	131	exbii 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ
133	129, 130, 132	3bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Succ
134	127, 133	anbi12ci 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod $/\$ Succ $/\$
135	88, 134	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 FullFun Apply pprod Succ $/\$
136	87, 135	orbi12i 523	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img $\/$ FullFun Apply pprod Succ $/\$ $\/$ $/\$
137	65, 136	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$
138	64, 137	orbi12i 523	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
139	56, 138	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . 24 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
140		onzsl 6631	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$
141		nlim0 5443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142		limeq 5397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143	141, 142	mtbiri 304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144	143	intnanrd 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
145		nsuceq0 5465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
146		neeq2 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
147	145, 146	mpbiri 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
148	147	necomd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
149	148	neneqd 2606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
150	149	nexdv 1775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
151	150	intnanrd 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
152		ioran 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
153	144, 151, 152	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$
154		orel2 384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
155	153, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
156		iftrue 3860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157		unisnif 30641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
158	156, 157	syl6eqr 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
159	158	eqeq2d 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
160	159	biimprd 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
161	160	adantld 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
162	155, 161	syld 45	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
163	159	biimpd 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	anc2li 559	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
165		orc 386	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
166	164, 165	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
167	162, 166	impbid 193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
168		neeq1 2663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
169	145, 168	mpbiri 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
170	169	neneqd 2606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	intnanrd 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
172	171	rexlimivw 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
173		orel1 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
174	172, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
175		nlimsucg 6627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
176	69, 175	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177		limeq 5397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	176, 177	mtbiri 304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179	178	rexlimivw 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180	179	intnanrd 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
181		orel1 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $/\$
182	180, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $/\$
183	145	neii 2603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	183	iffalsei 3864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185		iffalse 3863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	69, 175, 185	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	184, 186	eqtri 2450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188		eqeq1 2432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
189		unieq 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	fveq2d 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	177, 191	ifbieq2d 3879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	188, 192	ifbieq2d 3879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	187, 193, 191	3eqtr4a 2488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195	194	rexlimivw 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
196	195	eqeq2d 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
197	196	biimprd 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
198	197	adantld 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
199	174, 182, 198	3syld 57	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
200		rexex 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
201	196	biimpd 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202		olc 385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$
203	202	olcd 394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
204	200, 201, 203	syl6an 547	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
205	199, 204	impbid 193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
206	143	con2i 123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
207	206	intnanrd 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
208	207, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
209	178	exlimiv 1770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
210	209	con2i 123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
211	210	intnanrd 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
212		orel2 384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$ $/\$
213	211, 212	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$
214	206	iffalsed 3865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
215		iftrue 3860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
216	214, 215	eqtrd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
217	216	eqeq2d 2438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
218	217	biimprd 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
219	218	adantld 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
220	208, 213, 219	3syld 57	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
221	220	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
222	217	biimpd 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
223	222	anc2li 559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
224		orc 386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$
225	224	olcd 394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
226	223, 225	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
227	226	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
228	221, 227	impbid 193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
229	167, 205, 228	3jaoi 1327	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
230	140, 229	sylbi 198	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$ $/\$ $\/$ $/\$
231	139, 230	syl5bb 260	. . . . . . . . . . . . . . . . . . . . . . 23 Img FullFun Apply pprod Succ
232	55, 231	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Img FullFun Apply pprod Succ
233	27, 67	brcnv 4979	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply Apply
234	12, 41, 27	brapply 30654	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply
235	233, 234	bitri 252	. . . . . . . . . . . . . . . . . . . . . . 23 Apply
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Apply
237	232, 236	anbi12d 715	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
238		ancom 451	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
239	237, 238	syl6bb 264	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
240	239	exbidv 1762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
241		df-br 4367	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
242	67	elfix 30619	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
243	67, 67	brco 4967	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
244	241, 242, 243	3bitri 274	. . . . . . . . . . . . . . . . . . 19 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
245		fvex 5835	. . . . . . . . . . . . . . . . . . . 20
246	245	eqvinc 3141	. . . . . . . . . . . . . . . . . . 19 $/\$
247	240, 244, 246	3bitr4g 291	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
248	247	notbid 295	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
249	248	3expia 1207	. . . . . . . . . . . . . . . 16 $/\$ Apply Img FullFun Apply pprod Succ
250	249	pm5.32d 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ Apply Img FullFun Apply pprod Succ $/\$
251		annim 426	. . . . . . . . . . . . . . 15 $/\$
252	250, 251	syl6bb 264	. . . . . . . . . . . . . 14 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
253	53, 252	syl5bb 260	. . . . . . . . . . . . 13 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
254	253	exbidv 1762	. . . . . . . . . . . 12 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
255		exnal 1693	. . . . . . . . . . . 12
256	254, 255	syl6rbb 265	. . . . . . . . . . 11 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
257	12	eldm 4994	. . . . . . . . . . 11 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $\$ Apply Img FullFun Apply pprod Succ
258	256, 257	syl6bbr 266	. . . . . . . . . 10 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
259	258	con1bid 331	. . . . . . . . 9 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
260		df-ral 2719	. . . . . . . . 9
261	259, 260	syl6bbr 266	. . . . . . . 8 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
262	261	pm5.32i 641	. . . . . . 7 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
263		anass 653	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
264	262, 263	bitri 252	. . . . . 6 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
265	21, 39, 264	3bitri 274	. . . . 5 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
266	19, 20, 265	3bitr4ri 281	. . . 4 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
267	266	abbi2i 2543	. . 3 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
268	267	unieqi 4171	. 2 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
269	1, 268	eqtr4i 2453	1 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $\/$ w3o 981 $/\$ w3a 982

wal 1435

wceq 1437

wex 1657

wcel 1872

cab 2414

wne 2599

wral 2714

wrex 2715

cvv 3022 $\$ cdif 3376

cun 3377

cin 3378

c0 3704

cif 3854

csn 3941

cop 3947

cuni 4162 class class class wbr 4366

cep 4705

cid 4706

cxp 4794

ccnv 4795

cdm 4796

crn 4797

cres 4798

cima 4799

ccom 4800

con0 5385

wlim 5386

csuc 5387

wfun 5538

wfn 5539

cfv 5544

crdg 7082 pprodcpprod 30546

cbigcup 30549

cfix 30550

climits 30551

cfuns 30552 Imgcimg 30557 Domaincdomain 30558 Applycapply 30560 Succcsuccf 30563 FullFuncfullfn 30565

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408 ax-rep 4479 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-ral 2719 df-rex 2720 df-reu 2721 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-pss 3395 df-symdif 3636 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-tp 3946 df-op 3948 df-uni 4163 df-iun 4244 df-br 4367 df-opab 4426 df-mpt 4427 df-tr 4462 df-eprel 4707 df-id 4711 df-po 4717 df-so 4718 df-fr 4755 df-we 4757 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-pred 5342 df-ord 5388 df-on 5389 df-lim 5390 df-suc 5391 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-om 6651 df-1st 6751 df-2nd 6752 df-wrecs 6983 df-recs 7045 df-rdg 7083 df-txp 30569 df-pprod 30570 df-bigcup 30573 df-fix 30574 df-limits 30575 df-funs 30576 df-singleton 30577 df-singles 30578 df-image 30579 df-cart 30580 df-img 30581 df-domain 30582 df-cup 30584 df-succf 30587 df-apply 30588 df-funpart 30589 df-fullfun 30590

This theorem is referenced by: (None)

W3C validator