axcc2lem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axcc2lem		Structured version Visualization version GIF version

Theorem axcc2lem 10419

Description: Lemma for axcc2 10420. (Contributed by Mario Carneiro, 8-Feb-2013.)

**Hypotheses**
Ref	Expression
axcc2lem.1	⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
axcc2lem.2	⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
axcc2lem.3	⊢ 𝐺 = (𝑛 ∈ ω ↦ (2^nd ‘(𝑓‘(𝐴‘𝑛))))

**Assertion**
Ref	Expression
axcc2lem	⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Distinct variable groups: 𝐴,𝑓,𝑛 𝑓,𝐹,𝑔 𝑔,𝐺,𝑛 𝑛,𝐾 Allowed substitution hints: 𝐴(𝑔) 𝐹(𝑛) 𝐺(𝑓) 𝐾(𝑓,𝑔)

Proof of Theorem axcc2lem Dummy variables 𝑎 𝑧 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6894	. . . 4 ⊢ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V
2		axcc2lem.3	. . . 4 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2^nd ‘(𝑓‘(𝐴‘𝑛))))
3	1, 2	fnmpti 6678	. . 3 ⊢ 𝐺 Fn ω
4		vsnex 5406	. . . . . . . . . . . . . . 15 ⊢ {𝑛} ∈ V
5		fvex 6894	. . . . . . . . . . . . . . 15 ⊢ (𝐾‘𝑛) ∈ V
6	4, 5	xpex 7751	. . . . . . . . . . . . . 14 ⊢ ({𝑛} × (𝐾‘𝑛)) ∈ V
7		axcc2lem.2	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
8	7	fvmpt2 7001	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐾‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
9	6, 8	mpan2 703	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
10		vex 3457	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
11	10	snnz 4741	. . . . . . . . . . . . . 14 ⊢ {𝑛} ≠ ∅
12		0ex 5269	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
13	12	snnz 4741	. . . . . . . . . . . . . . . . 17 ⊢ {∅} ≠ ∅
14		iftrue 4492	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = {∅})
15	14	neeq1d 3015	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) = ∅ → (if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ ↔ {∅} ≠ ∅))
16	13, 15	mpbiri 261	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
17		iffalse 4495	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
18		neqne 2964	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ≠ ∅)
19	17, 18	eqnetrd 3023	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
20	16, 19	pm2.61i 184	. . . . . . . . . . . . . . 15 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅
21		p0ex 5355	. . . . . . . . . . . . . . . . . 18 ⊢ {∅} ∈ V
22		fvex 6894	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘𝑛) ∈ V
23	21, 22	ifex 4537	. . . . . . . . . . . . . . . . 17 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V
24		axcc2lem.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
25	24	fvmpt2 7001	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
26	23, 25	mpan2 703	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
27	26	neeq1d 3015	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝐾‘𝑛) ≠ ∅ ↔ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅))
28	20, 27	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) ≠ ∅)
29		xpnz 6156	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) ↔ ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
30	29	biimpi 219	. . . . . . . . . . . . . 14 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
31	11, 28, 30	sylancr 598	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
32	9, 31	eqnetrd 3023	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ≠ ∅)
33	6, 7	fnmpti 6678	. . . . . . . . . . . . . 14 ⊢ 𝐴 Fn ω
34		fnfvelrn 7075	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
35	33, 34	mpan 702	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ∈ ran 𝐴)
36		neeq1 3018	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑧 ≠ ∅ ↔ (𝐴‘𝑛) ≠ ∅))
37		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
38		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
39	37, 38	eleq12d 2855	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
40	36, 39	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
41	40	rspccv 3577	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝐴‘𝑛) ∈ ran 𝐴 → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
42	35, 41	syl5 35	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
43	32, 42	mpdi 46	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
44	43	impcom 412	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
45	9	eleq2d 2847	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
46	45	adantr 485	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
47	44, 46	mpbid 235	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))
48		xp2nd 8018	. . . . . . . . 9 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
49	47, 48	syl 18	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
50	49	3adant3 1148	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
51	2	fvmpt2 7001	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
52	1, 51	mpan2 703	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
53	52	3ad2ant1 1149	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
54	53	eqcomd 2767	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) = (𝐺‘𝑛))
55	26	3ad2ant1 1149	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
56		ifnefalse 4498	. . . . . . . . 9 ⊢ ((𝐹‘𝑛) ≠ ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
57	56	3ad2ant3 1151	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
58	55, 57	eqtrd 2796	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = (𝐹‘𝑛))
59	50, 54, 58	3eltr3d 2875	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
60	59	3expia 1137	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
61	60	expcom 418	. . . 4 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
62	61	ralrimiv 3154	. . 3 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
63		omex 9611	. . . . 5 ⊢ ω ∈ V
64		fnex 7215	. . . . 5 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
65	3, 63, 64	mp2an 704	. . . 4 ⊢ 𝐺 ∈ V
66		fneq1 6626	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
67		fveq1 6880	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
68	67	eleq1d 2846	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
69	68	imbi2d 343	. . . . . 6 ⊢ (𝑔 = 𝐺 → (((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
70	69	ralbidv 3186	. . . . 5 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
71	66, 70	anbi12d 643	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))))
72	65, 71	spcev 3564	. . 3 ⊢ ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
73	3, 62, 72	sylancr 598	. 2 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
74	6	a1i 11	. . . . . 6 ⊢ ((ω ∈ V ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐾‘𝑛)) ∈ V)
75	74, 7	fmptd 7109	. . . . 5 ⊢ (ω ∈ V → 𝐴:ω⟶V)
76	63, 75	ax-mp 5	. . . 4 ⊢ 𝐴:ω⟶V
77		sneq 4598	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
78		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐾‘𝑛) = (𝐾‘𝑘))
79	77, 78	xpeq12d 5692	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)))
80	79, 7, 6	fvmpt3i 6995	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
81	80	adantl 486	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
82	81	eqeq2d 2772	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘))))
83	9	adantr 485	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
84	83	eqeq1d 2763	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘))))
85		xp11 6173	. . . . . . . . . 10 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
86	11, 28, 85	sylancr 598	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
87	10	sneqr 4804	. . . . . . . . . 10 ⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘)
88	87	adantr 485	. . . . . . . . 9 ⊢ (({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)) → 𝑛 = 𝑘)
89	86, 88	biimtrdi 256	. . . . . . . 8 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
90	89	adantr 485	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
91	84, 90	sylbid 243	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
92	82, 91	sylbid 243	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
93	92	rgen2 3203	. . . 4 ⊢ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)
94		dff13 7252	. . . 4 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
95	76, 93, 94	mpbir2an 723	. . 3 ⊢ 𝐴:ω–1-1→V
96		f1f1orn 6832	. . . 4 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
97	63	f1oen 8968	. . . 4 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
98		ensym 8999	. . . 4 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
99	96, 97, 98	3syl 19	. . 3 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
100	7	rneqi 5927	. . . . 5 ⊢ ran 𝐴 = ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
101		dmmptg 6243	. . . . . . . 8 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐾‘𝑛)) ∈ V → dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω)
102	6	a1i 11	. . . . . . . 8 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ∈ V)
103	101, 102	mprg 3083	. . . . . . 7 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω
104	103, 63	eqeltri 2857	. . . . . 6 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
105		funmpt 6574	. . . . . 6 ⊢ Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
106		funrnex 7950	. . . . . 6 ⊢ (dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V → (Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) → ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V))
107	104, 105, 106	mp2 9	. . . . 5 ⊢ ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
108	100, 107	eqeltri 2857	. . . 4 ⊢ ran 𝐴 ∈ V
109		breq1 5111	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (𝑎 ≈ ω ↔ ran 𝐴 ≈ ω))
110		raleq 3318	. . . . . 6 ⊢ (𝑎 = ran 𝐴 → (∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
111	110	exbidv 1949	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
112	109, 111	imbi12d 347	. . . 4 ⊢ (𝑎 = ran 𝐴 → ((𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))))
113		ax-cc 10418	. . . 4 ⊢ (𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
114	108, 112, 113	vtocl 3524	. . 3 ⊢ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
115	95, 99, 114	mp2b 10	. 2 ⊢ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
116	73, 115	exlimiiv 1959	1 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∃wex 1807 ∈ wcel 2141 ≠ wne 2956 ∀wral 3077 Vcvv 3453 ∅c0 4285 ifcif 4486 {csn 4588 class class class wbr 5108 ↦ cmpt 5191 × cxp 5659 dom cdm 5661 ran crn 5662 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 –1-1-onto→wf1o 6535 ‘cfv 6536 ωcom 7861 2^nd c2nd 7984 ≈ cen 8939

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9609 ax-cc 10418

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-om 7862 df-2nd 7986 df-er 8693 df-en 8943

This theorem is referenced by: axcc2 10420

W3C validator