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 10505

Description: Lemma for axcc2 10506. (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 6933	. . . 4 ⊢ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V
2		axcc2lem.3	. . . 4 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2^nd ‘(𝑓‘(𝐴‘𝑛))))
3	1, 2	fnmpti 6723	. . 3 ⊢ 𝐺 Fn ω
4		vsnex 5449	. . . . . . . . . . . . . . 15 ⊢ {𝑛} ∈ V
5		fvex 6933	. . . . . . . . . . . . . . 15 ⊢ (𝐾‘𝑛) ∈ V
6	4, 5	xpex 7788	. . . . . . . . . . . . . 14 ⊢ ({𝑛} × (𝐾‘𝑛)) ∈ V
7		axcc2lem.2	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
8	7	fvmpt2 7040	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐾‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
9	6, 8	mpan2 690	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
10		vex 3492	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
11	10	snnz 4801	. . . . . . . . . . . . . 14 ⊢ {𝑛} ≠ ∅
12		0ex 5325	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
13	12	snnz 4801	. . . . . . . . . . . . . . . . 17 ⊢ {∅} ≠ ∅
14		iftrue 4554	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = {∅})
15	14	neeq1d 3006	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) = ∅ → (if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ ↔ {∅} ≠ ∅))
16	13, 15	mpbiri 258	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
17		iffalse 4557	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
18		neqne 2954	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ≠ ∅)
19	17, 18	eqnetrd 3014	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
20	16, 19	pm2.61i 182	. . . . . . . . . . . . . . 15 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅
21		p0ex 5402	. . . . . . . . . . . . . . . . . 18 ⊢ {∅} ∈ V
22		fvex 6933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘𝑛) ∈ V
23	21, 22	ifex 4598	. . . . . . . . . . . . . . . . 17 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V
24		axcc2lem.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
25	24	fvmpt2 7040	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
26	23, 25	mpan2 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
27	26	neeq1d 3006	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝐾‘𝑛) ≠ ∅ ↔ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅))
28	20, 27	mpbiri 258	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) ≠ ∅)
29		xpnz 6190	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) ↔ ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
30	29	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
31	11, 28, 30	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
32	9, 31	eqnetrd 3014	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ≠ ∅)
33	6, 7	fnmpti 6723	. . . . . . . . . . . . . 14 ⊢ 𝐴 Fn ω
34		fnfvelrn 7114	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
35	33, 34	mpan 689	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ∈ ran 𝐴)
36		neeq1 3009	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑧 ≠ ∅ ↔ (𝐴‘𝑛) ≠ ∅))
37		fveq2 6920	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
38		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
39	37, 38	eleq12d 2838	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
40	36, 39	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
41	40	rspccv 3632	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝐴‘𝑛) ∈ ran 𝐴 → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
42	35, 41	syl5 34	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
43	32, 42	mpdi 45	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
44	43	impcom 407	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
45	9	eleq2d 2830	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
46	45	adantr 480	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
47	44, 46	mpbid 232	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))
48		xp2nd 8063	. . . . . . . . 9 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
49	47, 48	syl 17	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
50	49	3adant3 1132	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
51	2	fvmpt2 7040	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
52	1, 51	mpan2 690	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
53	52	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
54	53	eqcomd 2746	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) = (𝐺‘𝑛))
55	26	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
56		ifnefalse 4560	. . . . . . . . 9 ⊢ ((𝐹‘𝑛) ≠ ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
57	56	3ad2ant3 1135	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
58	55, 57	eqtrd 2780	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = (𝐹‘𝑛))
59	50, 54, 58	3eltr3d 2858	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
60	59	3expia 1121	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
61	60	expcom 413	. . . 4 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
62	61	ralrimiv 3151	. . 3 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
63		omex 9712	. . . . 5 ⊢ ω ∈ V
64		fnex 7254	. . . . 5 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
65	3, 63, 64	mp2an 691	. . . 4 ⊢ 𝐺 ∈ V
66		fneq1 6670	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
67		fveq1 6919	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
68	67	eleq1d 2829	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
69	68	imbi2d 340	. . . . . 6 ⊢ (𝑔 = 𝐺 → (((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
70	69	ralbidv 3184	. . . . 5 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
71	66, 70	anbi12d 631	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))))
72	65, 71	spcev 3619	. . 3 ⊢ ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
73	3, 62, 72	sylancr 586	. 2 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
74	6	a1i 11	. . . . . 6 ⊢ ((ω ∈ V ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐾‘𝑛)) ∈ V)
75	74, 7	fmptd 7148	. . . . 5 ⊢ (ω ∈ V → 𝐴:ω⟶V)
76	63, 75	ax-mp 5	. . . 4 ⊢ 𝐴:ω⟶V
77		sneq 4658	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
78		fveq2 6920	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐾‘𝑛) = (𝐾‘𝑘))
79	77, 78	xpeq12d 5731	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)))
80	79, 7, 6	fvmpt3i 7034	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
81	80	adantl 481	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
82	81	eqeq2d 2751	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘))))
83	9	adantr 480	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
84	83	eqeq1d 2742	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘))))
85		xp11 6206	. . . . . . . . . 10 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
86	11, 28, 85	sylancr 586	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
87	10	sneqr 4865	. . . . . . . . . 10 ⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘)
88	87	adantr 480	. . . . . . . . 9 ⊢ (({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)) → 𝑛 = 𝑘)
89	86, 88	biimtrdi 253	. . . . . . . 8 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
90	89	adantr 480	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
91	84, 90	sylbid 240	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘))
92	82, 91	sylbid 240	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
93	92	rgen2 3205	. . . 4 ⊢ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)
94		dff13 7292	. . . 4 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
95	76, 93, 94	mpbir2an 710	. . 3 ⊢ 𝐴:ω–1-1→V
96		f1f1orn 6873	. . . 4 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
97	63	f1oen 9033	. . . 4 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
98		ensym 9063	. . . 4 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
99	96, 97, 98	3syl 18	. . 3 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
100	7	rneqi 5962	. . . . 5 ⊢ ran 𝐴 = ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
101		dmmptg 6273	. . . . . . . 8 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐾‘𝑛)) ∈ V → dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω)
102	6	a1i 11	. . . . . . . 8 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ∈ V)
103	101, 102	mprg 3073	. . . . . . 7 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω
104	103, 63	eqeltri 2840	. . . . . 6 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
105		funmpt 6616	. . . . . 6 ⊢ Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
106		funrnex 7994	. . . . . 6 ⊢ (dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V → (Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) → ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V))
107	104, 105, 106	mp2 9	. . . . 5 ⊢ ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
108	100, 107	eqeltri 2840	. . . 4 ⊢ ran 𝐴 ∈ V
109		breq1 5169	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (𝑎 ≈ ω ↔ ran 𝐴 ≈ ω))
110		raleq 3331	. . . . . 6 ⊢ (𝑎 = ran 𝐴 → (∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
111	110	exbidv 1920	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
112	109, 111	imbi12d 344	. . . 4 ⊢ (𝑎 = ran 𝐴 → ((𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))))
113		ax-cc 10504	. . . 4 ⊢ (𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
114	108, 112, 113	vtocl 3570	. . 3 ⊢ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
115	95, 99, 114	mp2b 10	. 2 ⊢ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
116	73, 115	exlimiiv 1930	1 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∃wex 1777 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 Vcvv 3488 ∅c0 4352 ifcif 4548 {csn 4648 class class class wbr 5166 ↦ cmpt 5249 × cxp 5698 dom cdm 5700 ran crn 5701 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 –1-1→wf1 6570 –1-1-onto→wf1o 6572 ‘cfv 6573 ωcom 7903 2^nd c2nd 8029 ≈ cen 9000

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cc 10504

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-om 7904 df-2nd 8031 df-er 8763 df-en 9004

This theorem is referenced by: axcc2 10506

W3C validator