ac6s6 - Mathbox for Giovanni Mascellani

	Mathbox for Giovanni Mascellani	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ac6s6		Structured version Unicode version

Theorem ac6s6 29007

Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)

**Hypotheses**
Ref	Expression
ac6s6.1
ac6s6.2
ac6s6.3

**Assertion**
Ref	Expression
ac6s6

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem ac6s6**
Step	Hyp	Ref	Expression
1		hbe1 1777	. . . . . 6
2		iftrue 3816	. . . . . . 7
3	2	abeq2d 2553	. . . . . 6
4	1, 3	exbidh 1643	. . . . 5
5	4	ibir 242	. . . 4
6		vex 2994	. . . . . 6
7	6	exiftru 1711	. . . . 5
8	1	hbn 1829	. . . . . 6
9		iffalse 3818	. . . . . . 7
10	9	eleq2d 2510	. . . . . 6
11	8, 10	exbidh 1643	. . . . 5
12	7, 11	mpbiri 233	. . . 4
13	5, 12	pm2.61i 164	. . 3
14	13	rgenw 2802	. 2
15		nfe1 1778	. . . 4
16		ac6s6.1	. . . 4
17	15, 16	nfim 1853	. . 3
18		ac6s6.2	. . 3
19		ac6s6.3	. . . . . 6
20		id 22	. . . . . . . . . . . . . . 15
21	20	a1i 11	. . . . . . . . . . . . . 14
22		ax-1 6	. . . . . . . . . . . . . . . . . . 19
23		tsim3 28966	. . . . . . . . . . . . . . . . . . . 20 $\/$
24	23	a1d 25	. . . . . . . . . . . . . . . . . . 19 $\/$
25	22, 24	cnf2dd 28917	. . . . . . . . . . . . . . . . . 18
26		tsim3 28966	. . . . . . . . . . . . . . . . . . 19 $\/$
27	26	a1d 25	. . . . . . . . . . . . . . . . . 18 $\/$
28	25, 27	cnf2dd 28917	. . . . . . . . . . . . . . . . 17
29		tsim2 28965	. . . . . . . . . . . . . . . . . 18 $\/$
30	29	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$
31	28, 30	cnf2dd 28917	. . . . . . . . . . . . . . . 16
32		tsim2 28965	. . . . . . . . . . . . . . . . . 18 $\/$
33	32	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$
34	25, 33	cnf2dd 28917	. . . . . . . . . . . . . . . 16
35	31, 34	mpdd 40	. . . . . . . . . . . . . . 15
36		tsbi4 28970	. . . . . . . . . . . . . . . 16 $\/$ $\/$
37	36	a1d 25	. . . . . . . . . . . . . . 15 $\/$ $\/$
38	35, 37	cnfn2dd 28919	. . . . . . . . . . . . . 14 $\/$
39	21, 38	cnf2dd 28917	. . . . . . . . . . . . 13
40		tsim3 28966	. . . . . . . . . . . . . . . . 17 $\/$
41	40	a1d 25	. . . . . . . . . . . . . . . 16 $\/$
42	28, 41	cnf2dd 28917	. . . . . . . . . . . . . . 15
43		tsim3 28966	. . . . . . . . . . . . . . . 16 $\/$
44	43	a1d 25	. . . . . . . . . . . . . . 15 $\/$
45	42, 44	cnf2dd 28917	. . . . . . . . . . . . . 14
46		tsbi2 28968	. . . . . . . . . . . . . . 15 $\/$ $\/$
47	46	a1d 25	. . . . . . . . . . . . . 14 $\/$ $\/$
48	45, 47	cnf2dd 28917	. . . . . . . . . . . . 13 $\/$
49	39, 48	cnf1dd 28916	. . . . . . . . . . . 12
50		tsim2 28965	. . . . . . . . . . . . . . . . . . 19 $\/$
51	50	a1d 25	. . . . . . . . . . . . . . . . . 18 $\/$
52	42, 51	cnf2dd 28917	. . . . . . . . . . . . . . . . 17
53		simplim 151	. . . . . . . . . . . . . . . . 17
54	52, 53	syld 44	. . . . . . . . . . . . . . . 16
55		tsbi3 28969	. . . . . . . . . . . . . . . . 17 $\/$ $\/$
56	55	a1d 25	. . . . . . . . . . . . . . . 16 $\/$ $\/$
57	54, 56	cnfn2dd 28919	. . . . . . . . . . . . . . 15 $\/$
58	21, 57	cnf1dd 28916	. . . . . . . . . . . . . 14
59		tsim1 28964	. . . . . . . . . . . . . . . 16 $\/$ $\/$
60	59	a1d 25	. . . . . . . . . . . . . . 15 $\/$ $\/$
61	60	or32dd 28920	. . . . . . . . . . . . . 14 $\/$ $\/$
62	58, 61	cnf2dd 28917	. . . . . . . . . . . . 13 $\/$
63	31, 62	cnfn1dd 28918	. . . . . . . . . . . 12
64	49, 63	contrd 28923	. . . . . . . . . . 11
65	64	a1d 25	. . . . . . . . . 10
66		ax-1 6	. . . . . . . . . . . . . . 15
67	23	a1d 25	. . . . . . . . . . . . . . 15 $\/$
68	66, 67	cnf2dd 28917	. . . . . . . . . . . . . 14
69	26	a1d 25	. . . . . . . . . . . . . 14 $\/$
70	68, 69	cnf2dd 28917	. . . . . . . . . . . . 13
71	29	a1d 25	. . . . . . . . . . . . 13 $\/$
72	70, 71	cnf2dd 28917	. . . . . . . . . . . 12
73	32	a1d 25	. . . . . . . . . . . . 13 $\/$
74	68, 73	cnf2dd 28917	. . . . . . . . . . . 12
75	72, 74	mpdd 40	. . . . . . . . . . 11
76		tsbi3 28969	. . . . . . . . . . . 12 $\/$ $\/$
77	76	a1d 25	. . . . . . . . . . 11 $\/$ $\/$
78	75, 77	cnfn2dd 28919	. . . . . . . . . 10 $\/$
79	65, 78	cnfn2dd 28919	. . . . . . . . 9
80	40	a1d 25	. . . . . . . . . . . . . . . 16 $\/$
81	70, 80	cnf2dd 28917	. . . . . . . . . . . . . . 15
82	50	a1d 25	. . . . . . . . . . . . . . 15 $\/$
83	81, 82	cnf2dd 28917	. . . . . . . . . . . . . 14
84	83, 53	syld 44	. . . . . . . . . . . . 13
85		tsbi4 28970	. . . . . . . . . . . . . 14 $\/$ $\/$
86	85	a1d 25	. . . . . . . . . . . . 13 $\/$ $\/$
87	84, 86	cnfn2dd 28919	. . . . . . . . . . . 12 $\/$
88	65, 87	cnfn1dd 28918	. . . . . . . . . . 11
89	88	a1dd 46	. . . . . . . . . 10
90		tsbi1 28967	. . . . . . . . . . . 12 $\/$ $\/$
91	90	a1d 25	. . . . . . . . . . 11 $\/$ $\/$
92	91	or32dd 28920	. . . . . . . . . 10 $\/$ $\/$
93	89, 92	cnfn2dd 28919	. . . . . . . . 9 $\/$
94	79, 93	cnfn1dd 28918	. . . . . . . 8
95	43	a1d 25	. . . . . . . . 9 $\/$
96	81, 95	cnf2dd 28917	. . . . . . . 8
97	94, 96	contrd 28923	. . . . . . 7
98	97	efald2 28901	. . . . . 6
99	19, 98	ax-mp 5	. . . . 5
100	3, 99	ax-mp 5	. . . 4
101	6	a1i 11	. . . . . . 7
102		id 22	. . . . . . . . . . . 12
103		tsim2 28965	. . . . . . . . . . . . . . 15 $\/$
104	103	ord 377	. . . . . . . . . . . . . 14
105	104	a1dd 46	. . . . . . . . . . . . 13
106	105	a1dd 46	. . . . . . . . . . . 12
107	102, 106	mt3d 125	. . . . . . . . . . 11
108	107	a1d 25	. . . . . . . . . 10
109		simplim 151	. . . . . . . . . 10
110	108, 109	syld 44	. . . . . . . . 9
111		tsim2 28965	. . . . . . . . . . . . . 14 $\/$
112	111	ord 377	. . . . . . . . . . . . 13
113	112	a1dd 46	. . . . . . . . . . . 12
114	102, 113	mt3d 125	. . . . . . . . . . 11
115	108, 114	syld 44	. . . . . . . . . 10
116		id 22	. . . . . . . . . . . . . . . . . 18 $\/$ $\/$
117	116	notornotel2 28922	. . . . . . . . . . . . . . . . 17 $\/$
118	117	a1i 11	. . . . . . . . . . . . . . . 16 $\/$
119	116	notornotel1 28921	. . . . . . . . . . . . . . . . . 18 $\/$
120	119	a1i 11	. . . . . . . . . . . . . . . . 17 $\/$
121		tsbi3 28969	. . . . . . . . . . . . . . . . . 18 $\/$ $\/$
122	121	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$ $\/$ $\/$
123	120, 122	cnfn2dd 28919	. . . . . . . . . . . . . . . 16 $\/$ $\/$
124	118, 123	cnfn2dd 28919	. . . . . . . . . . . . . . 15 $\/$
125		a1tru 1385	. . . . . . . . . . . . . . . . 17
126	125	a1d 25	. . . . . . . . . . . . . . . 16 $\/$
127		tsbi1 28967	. . . . . . . . . . . . . . . . . 18 $\/$ $\/$
128	127	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$ $\/$ $\/$
129	128	or32dd 28920	. . . . . . . . . . . . . . . 16 $\/$ $\/$ $\/$
130	126, 129	cnfn2dd 28919	. . . . . . . . . . . . . . 15 $\/$ $\/$
131	124, 130	cnfn1dd 28918	. . . . . . . . . . . . . 14 $\/$
132	131	a1dd 46	. . . . . . . . . . . . 13 $\/$
133	132	a1dd 46	. . . . . . . . . . . 12 $\/$
134		ax-1 6	. . . . . . . . . . . . 13 $\/$
135		tsim3 28966	. . . . . . . . . . . . . 14 $\/$
136	135	a1d 25	. . . . . . . . . . . . 13 $\/$ $\/$
137	134, 136	cnf2dd 28917	. . . . . . . . . . . 12 $\/$
138	133, 137	contrd 28923	. . . . . . . . . . 11 $\/$
139	138	a1d 25	. . . . . . . . . 10 $\/$
140	115, 139	cnfn1dd 28918	. . . . . . . . 9
141	110, 140	contrd 28923	. . . . . . . 8
142	141	efald2 28901	. . . . . . 7
143	101, 142	ax-mp 5	. . . . . 6
144	10, 143	ax-mp 5	. . . . 5
145		ax-1 6	. . . . . . . . . 10