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 10356

Description: Lemma for axcc2 10357. (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 6847	. . . 4 ⊢ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V
2		axcc2lem.3	. . . 4 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2^nd ‘(𝑓‘(𝐴‘𝑛))))
3	1, 2	fnmpti 6635	. . 3 ⊢ 𝐺 Fn ω
4		vsnex 5371	. . . . . . . . . . . . . . 15 ⊢ {𝑛} ∈ V
5		fvex 6847	. . . . . . . . . . . . . . 15 ⊢ (𝐾‘𝑛) ∈ V
6	4, 5	xpex 7703	. . . . . . . . . . . . . 14 ⊢ ({𝑛} × (𝐾‘𝑛)) ∈ V
7		axcc2lem.2	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
8	7	fvmpt2 6954	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐾‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
9	6, 8	mpan2 697	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
10		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
11	10	snnz 4715	. . . . . . . . . . . . . 14 ⊢ {𝑛} ≠ ∅
12		0ex 5236	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
13	12	snnz 4715	. . . . . . . . . . . . . . . . 17 ⊢ {∅} ≠ ∅
14		iftrue 4467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = {∅})
15	14	neeq1d 2994	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) = ∅ → (if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ ↔ {∅} ≠ ∅))
16	13, 15	mpbiri 259	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
17		iffalse 4470	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
18		neqne 2943	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ≠ ∅)
19	17, 18	eqnetrd 3002	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
20	16, 19	pm2.61i 183	. . . . . . . . . . . . . . 15 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅
21		p0ex 5320	. . . . . . . . . . . . . . . . . 18 ⊢ {∅} ∈ V
22		fvex 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘𝑛) ∈ V
23	21, 22	ifex 4512	. . . . . . . . . . . . . . . . 17 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V
24		axcc2lem.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
25	24	fvmpt2 6954	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
26	23, 25	mpan2 697	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
27	26	neeq1d 2994	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝐾‘𝑛) ≠ ∅ ↔ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅))
28	20, 27	mpbiri 259	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) ≠ ∅)
29		xpnz 6117	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) ↔ ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
30	29	biimpi 217	. . . . . . . . . . . . . 14 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
31	11, 28, 30	sylancr 593	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
32	9, 31	eqnetrd 3002	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ≠ ∅)
33	6, 7	fnmpti 6635	. . . . . . . . . . . . . 14 ⊢ 𝐴 Fn ω
34		fnfvelrn 7028	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
35	33, 34	mpan 696	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ∈ ran 𝐴)
36		neeq1 2997	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑧 ≠ ∅ ↔ (𝐴‘𝑛) ≠ ∅))
37		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
38		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
39	37, 38	eleq12d 2834	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
40	36, 39	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
41	40	rspccv 3564	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝐴‘𝑛) ∈ ran 𝐴 → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
42	35, 41	syl5 34	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
43	32, 42	mpdi 45	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
44	43	impcom 408	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
45	9	eleq2d 2826	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
46	45	adantr 481	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
47	44, 46	mpbid 233	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))
48		xp2nd 7971	. . . . . . . . 9 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
49	47, 48	syl 17	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
50	49	3adant3 1138	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
51	2	fvmpt2 6954	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
52	1, 51	mpan2 697	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
53	52	3ad2ant1 1139	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
54	53	eqcomd 2746	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) = (𝐺‘𝑛))
55	26	3ad2ant1 1139	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
56		ifnefalse 4473	. . . . . . . . 9 ⊢ ((𝐹‘𝑛) ≠ ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
57	56	3ad2ant3 1141	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
58	55, 57	eqtrd 2775	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = (𝐹‘𝑛))
59	50, 54, 58	3eltr3d 2854	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
60	59	3expia 1127	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
61	60	expcom 414	. . . 4 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
62	61	ralrimiv 3131	. . 3 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
63		omex 9562	. . . . 5 ⊢ ω ∈ V
64		fnex 7168	. . . . 5 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
65	3, 63, 64	mp2an 698	. . . 4 ⊢ 𝐺 ∈ V
66		fneq1 6583	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
67		fveq1 6833	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
68	67	eleq1d 2825	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
69	68	imbi2d 341	. . . . . 6 ⊢ (𝑔 = 𝐺 → (((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
70	69	ralbidv 3163	. . . . 5 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
71	66, 70	anbi12d 638	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))))
72	65, 71	spcev 3551	. . 3 ⊢ ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
73	3, 62, 72	sylancr 593	. 2 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
74	6	a1i 11	. . . . . 6 ⊢ ((ω ∈ V ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐾‘𝑛)) ∈ V)
75	74, 7	fmptd 7062	. . . . 5 ⊢ (ω ∈ V → 𝐴:ω⟶V)
76	63, 75	ax-mp 5	. . . 4 ⊢ 𝐴:ω⟶V
77		sneq 4572	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
78		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐾‘𝑛) = (𝐾‘𝑘))
79	77, 78	xpeq12d 5656	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)))
80	79, 7, 6	fvmpt3i 6948	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
81	80	adantl 482	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
82	81	eqeq2d 2751	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘))))
83	9	adantr 481	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
84	83	eqeq1d 2742	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘))))
85		xp11 6133	. . . . . . . . . 10 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
86	11, 28, 85	sylancr 593	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
87	10	sneqr 4778	. . . . . . . . . 10 ⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘)
88	87	adantr 481	. . . . . . . . 9 ⊢ (({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)) → 𝑛 = 𝑘)
89	86, 88	biimtrdi 254	. . . . . . . 8 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
90	89	adantr 481	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
91	84, 90	sylbid 241	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
92	82, 91	sylbid 241	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
93	92	rgen2 3180	. . . 4 ⊢ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)
94		dff13 7205	. . . 4 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
95	76, 93, 94	mpbir2an 717	. . 3 ⊢ 𝐴:ω–1-1→V
96		f1f1orn 6785	. . . 4 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
97	63	f1oen 8916	. . . 4 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
98		ensym 8947	. . . 4 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
99	96, 97, 98	3syl 18	. . 3 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
100	7	rneqi 5886	. . . . 5 ⊢ ran 𝐴 = ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
101		dmmptg 6200	. . . . . . . 8 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐾‘𝑛)) ∈ V → dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω)
102	6	a1i 11	. . . . . . . 8 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ∈ V)
103	101, 102	mprg 3060	. . . . . . 7 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω
104	103, 63	eqeltri 2836	. . . . . 6 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
105		funmpt 6530	. . . . . 6 ⊢ Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
106		funrnex 7903	. . . . . 6 ⊢ (dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V → (Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) → ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V))
107	104, 105, 106	mp2 9	. . . . 5 ⊢ ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
108	100, 107	eqeltri 2836	. . . 4 ⊢ ran 𝐴 ∈ V
109		breq1 5082	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (𝑎 ≈ ω ↔ ran 𝐴 ≈ ω))
110		raleq 3295	. . . . . 6 ⊢ (𝑎 = ran 𝐴 → (∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
111	110	exbidv 1928	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
112	109, 111	imbi12d 345	. . . 4 ⊢ (𝑎 = ran 𝐴 → ((𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))))
113		ax-cc 10355	. . . 4 ⊢ (𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
114	108, 112, 113	vtocl 3506	. . 3 ⊢ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
115	95, 99, 114	mp2b 10	. 2 ⊢ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
116	73, 115	exlimiiv 1938	1 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∃wex 1786 ∈ wcel 2119 ≠ wne 2935 ∀wral 3054 Vcvv 3432 ∅c0 4268 ifcif 4461 {csn 4562 class class class wbr 5079 ↦ cmpt 5160 × cxp 5623 dom cdm 5625 ran crn 5626 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 –1-1→wf1 6489 –1-1-onto→wf1o 6491 ‘cfv 6492 ωcom 7813 2^nd c2nd 7937 ≈ cen 8887

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-inf2 9560 ax-cc 10355

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-om 7814 df-2nd 7939 df-er 8640 df-en 8891

This theorem is referenced by: axcc2 10357

W3C validator