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 10469

Description: Lemma for axcc2 10470. (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 6915	. . . 4 ⊢ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V
2		axcc2lem.3	. . . 4 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2^nd ‘(𝑓‘(𝐴‘𝑛))))
3	1, 2	fnmpti 6703	. . 3 ⊢ 𝐺 Fn ω
4		vsnex 5435	. . . . . . . . . . . . . . 15 ⊢ {𝑛} ∈ V
5		fvex 6915	. . . . . . . . . . . . . . 15 ⊢ (𝐾‘𝑛) ∈ V
6	4, 5	xpex 7763	. . . . . . . . . . . . . 14 ⊢ ({𝑛} × (𝐾‘𝑛)) ∈ V
7		axcc2lem.2	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
8	7	fvmpt2 7021	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐾‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
9	6, 8	mpan2 689	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
10		vex 3477	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
11	10	snnz 4785	. . . . . . . . . . . . . 14 ⊢ {𝑛} ≠ ∅
12		0ex 5311	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
13	12	snnz 4785	. . . . . . . . . . . . . . . . 17 ⊢ {∅} ≠ ∅
14		iftrue 4538	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = {∅})
15	14	neeq1d 2997	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) = ∅ → (if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ ↔ {∅} ≠ ∅))
16	13, 15	mpbiri 257	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
17		iffalse 4541	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
18		neqne 2945	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ≠ ∅)
19	17, 18	eqnetrd 3005	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
20	16, 19	pm2.61i 182	. . . . . . . . . . . . . . 15 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅
21		p0ex 5388	. . . . . . . . . . . . . . . . . 18 ⊢ {∅} ∈ V
22		fvex 6915	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘𝑛) ∈ V
23	21, 22	ifex 4582	. . . . . . . . . . . . . . . . 17 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V
24		axcc2lem.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
25	24	fvmpt2 7021	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
26	23, 25	mpan2 689	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
27	26	neeq1d 2997	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝐾‘𝑛) ≠ ∅ ↔ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅))
28	20, 27	mpbiri 257	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) ≠ ∅)
29		xpnz 6168	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) ↔ ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
30	29	biimpi 215	. . . . . . . . . . . . . 14 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
31	11, 28, 30	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
32	9, 31	eqnetrd 3005	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ≠ ∅)
33	6, 7	fnmpti 6703	. . . . . . . . . . . . . 14 ⊢ 𝐴 Fn ω
34		fnfvelrn 7095	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
35	33, 34	mpan 688	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ∈ ran 𝐴)
36		neeq1 3000	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑧 ≠ ∅ ↔ (𝐴‘𝑛) ≠ ∅))
37		fveq2 6902	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
38		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
39	37, 38	eleq12d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
40	36, 39	imbi12d 343	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
41	40	rspccv 3608	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝐴‘𝑛) ∈ ran 𝐴 → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
42	35, 41	syl5 34	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
43	32, 42	mpdi 45	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
44	43	impcom 406	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
45	9	eleq2d 2815	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
46	45	adantr 479	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
47	44, 46	mpbid 231	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))
48		xp2nd 8034	. . . . . . . . 9 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
49	47, 48	syl 17	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
50	49	3adant3 1129	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
51	2	fvmpt2 7021	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
52	1, 51	mpan2 689	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
53	52	3ad2ant1 1130	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
54	53	eqcomd 2734	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) = (𝐺‘𝑛))
55	26	3ad2ant1 1130	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
56		ifnefalse 4544	. . . . . . . . 9 ⊢ ((𝐹‘𝑛) ≠ ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
57	56	3ad2ant3 1132	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
58	55, 57	eqtrd 2768	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = (𝐹‘𝑛))
59	50, 54, 58	3eltr3d 2843	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
60	59	3expia 1118	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
61	60	expcom 412	. . . 4 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
62	61	ralrimiv 3142	. . 3 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
63		omex 9676	. . . . 5 ⊢ ω ∈ V
64		fnex 7235	. . . . 5 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
65	3, 63, 64	mp2an 690	. . . 4 ⊢ 𝐺 ∈ V
66		fneq1 6650	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
67		fveq1 6901	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
68	67	eleq1d 2814	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
69	68	imbi2d 339	. . . . . 6 ⊢ (𝑔 = 𝐺 → (((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
70	69	ralbidv 3175	. . . . 5 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
71	66, 70	anbi12d 630	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))))
72	65, 71	spcev 3595	. . 3 ⊢ ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
73	3, 62, 72	sylancr 585	. 2 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
74	6	a1i 11	. . . . . 6 ⊢ ((ω ∈ V ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐾‘𝑛)) ∈ V)
75	74, 7	fmptd 7129	. . . . 5 ⊢ (ω ∈ V → 𝐴:ω⟶V)
76	63, 75	ax-mp 5	. . . 4 ⊢ 𝐴:ω⟶V
77		sneq 4642	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
78		fveq2 6902	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐾‘𝑛) = (𝐾‘𝑘))
79	77, 78	xpeq12d 5713	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)))
80	79, 7, 6	fvmpt3i 7015	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
81	80	adantl 480	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
82	81	eqeq2d 2739	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘))))
83	9	adantr 479	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
84	83	eqeq1d 2730	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘))))
85		xp11 6184	. . . . . . . . . 10 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
86	11, 28, 85	sylancr 585	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
87	10	sneqr 4846	. . . . . . . . . 10 ⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘)
88	87	adantr 479	. . . . . . . . 9 ⊢ (({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)) → 𝑛 = 𝑘)
89	86, 88	biimtrdi 252	. . . . . . . 8 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
90	89	adantr 479	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
91	84, 90	sylbid 239	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
92	82, 91	sylbid 239	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
93	92	rgen2 3195	. . . 4 ⊢ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)
94		dff13 7271	. . . 4 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
95	76, 93, 94	mpbir2an 709	. . 3 ⊢ 𝐴:ω–1-1→V
96		f1f1orn 6855	. . . 4 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
97	63	f1oen 9002	. . . 4 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
98		ensym 9032	. . . 4 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
99	96, 97, 98	3syl 18	. . 3 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
100	7	rneqi 5943	. . . . 5 ⊢ ran 𝐴 = ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
101		dmmptg 6251	. . . . . . . 8 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐾‘𝑛)) ∈ V → dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω)
102	6	a1i 11	. . . . . . . 8 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ∈ V)
103	101, 102	mprg 3064	. . . . . . 7 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω
104	103, 63	eqeltri 2825	. . . . . 6 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
105		funmpt 6596	. . . . . 6 ⊢ Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
106		funrnex 7965	. . . . . 6 ⊢ (dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V → (Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) → ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V))
107	104, 105, 106	mp2 9	. . . . 5 ⊢ ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
108	100, 107	eqeltri 2825	. . . 4 ⊢ ran 𝐴 ∈ V
109		breq1 5155	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (𝑎 ≈ ω ↔ ran 𝐴 ≈ ω))
110		raleq 3320	. . . . . 6 ⊢ (𝑎 = ran 𝐴 → (∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
111	110	exbidv 1916	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
112	109, 111	imbi12d 343	. . . 4 ⊢ (𝑎 = ran 𝐴 → ((𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))))
113		ax-cc 10468	. . . 4 ⊢ (𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
114	108, 112, 113	vtocl 3545	. . 3 ⊢ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
115	95, 99, 114	mp2b 10	. 2 ⊢ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
116	73, 115	exlimiiv 1926	1 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ≠ wne 2937 ∀wral 3058 Vcvv 3473 ∅c0 4326 ifcif 4532 {csn 4632 class class class wbr 5152 ↦ cmpt 5235 × cxp 5680 dom cdm 5682 ran crn 5683 Fun wfun 6547 Fn wfn 6548 ⟶wf 6549 –1-1→wf1 6550 –1-1-onto→wf1o 6552 ‘cfv 6553 ωcom 7878 2^nd c2nd 8000 ≈ cen 8969

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 ax-rep 5289 ax-sep 5303 ax-nul 5310 ax-pow 5369 ax-pr 5433 ax-un 7748 ax-inf2 9674 ax-cc 10468

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-ral 3059 df-rex 3068 df-reu 3375 df-rab 3431 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4327 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-iun 5002 df-br 5153 df-opab 5215 df-mpt 5236 df-tr 5270 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-ord 6377 df-on 6378 df-lim 6379 df-suc 6380 df-iota 6505 df-fun 6555 df-fn 6556 df-f 6557 df-f1 6558 df-fo 6559 df-f1o 6560 df-fv 6561 df-om 7879 df-2nd 8002 df-er 8733 df-en 8973

This theorem is referenced by: axcc2 10470

W3C validator