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 10474

Description: Lemma for axcc2 10475. (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 6920	. . . 4 ⊢ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V
2		axcc2lem.3	. . . 4 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2^nd ‘(𝑓‘(𝐴‘𝑛))))
3	1, 2	fnmpti 6712	. . 3 ⊢ 𝐺 Fn ω
4		vsnex 5440	. . . . . . . . . . . . . . 15 ⊢ {𝑛} ∈ V
5		fvex 6920	. . . . . . . . . . . . . . 15 ⊢ (𝐾‘𝑛) ∈ V
6	4, 5	xpex 7772	. . . . . . . . . . . . . 14 ⊢ ({𝑛} × (𝐾‘𝑛)) ∈ V
7		axcc2lem.2	. . . . . . . . . . . . . . 15 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
8	7	fvmpt2 7027	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐾‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
9	6, 8	mpan2 691	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
10		vex 3482	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
11	10	snnz 4781	. . . . . . . . . . . . . 14 ⊢ {𝑛} ≠ ∅
12		0ex 5313	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
13	12	snnz 4781	. . . . . . . . . . . . . . . . 17 ⊢ {∅} ≠ ∅
14		iftrue 4537	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = {∅})
15	14	neeq1d 2998	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) = ∅ → (if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ ↔ {∅} ≠ ∅))
16	13, 15	mpbiri 258	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
17		iffalse 4540	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
18		neqne 2946	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ≠ ∅)
19	17, 18	eqnetrd 3006	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)
20	16, 19	pm2.61i 182	. . . . . . . . . . . . . . 15 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅
21		p0ex 5390	. . . . . . . . . . . . . . . . . 18 ⊢ {∅} ∈ V
22		fvex 6920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹‘𝑛) ∈ V
23	21, 22	ifex 4581	. . . . . . . . . . . . . . . . 17 ⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V
24		axcc2lem.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
25	24	fvmpt2 7027	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
26	23, 25	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
27	26	neeq1d 2998	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝐾‘𝑛) ≠ ∅ ↔ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅))
28	20, 27	mpbiri 258	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝐾‘𝑛) ≠ ∅)
29		xpnz 6181	. . . . . . . . . . . . . . 15 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) ↔ ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
30	29	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
31	11, 28, 30	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ≠ ∅)
32	9, 31	eqnetrd 3006	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ≠ ∅)
33	6, 7	fnmpti 6712	. . . . . . . . . . . . . 14 ⊢ 𝐴 Fn ω
34		fnfvelrn 7100	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
35	33, 34	mpan 690	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ∈ ran 𝐴)
36		neeq1 3001	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑧 ≠ ∅ ↔ (𝐴‘𝑛) ≠ ∅))
37		fveq2 6907	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
38		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
39	37, 38	eleq12d 2833	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
40	36, 39	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))))
41	40	rspccv 3619	. . . . . . . . . . . . 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 2825	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
46	45	adantr 480	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))))
47	44, 46	mpbid 232	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))
48		xp2nd 8046	. . . . . . . . 9 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
49	47, 48	syl 17	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
50	49	3adant3 1131	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛))
51	2	fvmpt2 7027	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ (2^nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
52	1, 51	mpan2 691	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
53	52	3ad2ant1 1132	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) = (2^nd ‘(𝑓‘(𝐴‘𝑛))))
54	53	eqcomd 2741	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2^nd ‘(𝑓‘(𝐴‘𝑛))) = (𝐺‘𝑛))
55	26	3ad2ant1 1132	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)))
56		ifnefalse 4543	. . . . . . . . 9 ⊢ ((𝐹‘𝑛) ≠ ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
57	56	3ad2ant3 1134	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛))
58	55, 57	eqtrd 2775	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = (𝐹‘𝑛))
59	50, 54, 58	3eltr3d 2853	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
60	59	3expia 1120	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
61	60	expcom 413	. . . 4 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
62	61	ralrimiv 3143	. . 3 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
63		omex 9681	. . . . 5 ⊢ ω ∈ V
64		fnex 7237	. . . . 5 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
65	3, 63, 64	mp2an 692	. . . 4 ⊢ 𝐺 ∈ V
66		fneq1 6660	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
67		fveq1 6906	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
68	67	eleq1d 2824	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
69	68	imbi2d 340	. . . . . 6 ⊢ (𝑔 = 𝐺 → (((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
70	69	ralbidv 3176	. . . . 5 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
71	66, 70	anbi12d 632	. . . 4 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))))
72	65, 71	spcev 3606	. . 3 ⊢ ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
73	3, 62, 72	sylancr 587	. 2 ⊢ (∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
74	6	a1i 11	. . . . . 6 ⊢ ((ω ∈ V ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐾‘𝑛)) ∈ V)
75	74, 7	fmptd 7134	. . . . 5 ⊢ (ω ∈ V → 𝐴:ω⟶V)
76	63, 75	ax-mp 5	. . . 4 ⊢ 𝐴:ω⟶V
77		sneq 4641	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
78		fveq2 6907	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐾‘𝑛) = (𝐾‘𝑘))
79	77, 78	xpeq12d 5720	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)))
80	79, 7, 6	fvmpt3i 7021	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
81	80	adantl 481	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘)))
82	81	eqeq2d 2746	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘))))
83	9	adantr 480	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛)))
84	83	eqeq1d 2737	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘))))
85		xp11 6197	. . . . . . . . . 10 ⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
86	11, 28, 85	sylancr 587	. . . . . . . . 9 ⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘))))
87	10	sneqr 4845	. . . . . . . . . 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 3197	. . . 4 ⊢ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)
94		dff13 7275	. . . 4 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
95	76, 93, 94	mpbir2an 711	. . 3 ⊢ 𝐴:ω–1-1→V
96		f1f1orn 6860	. . . 4 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
97	63	f1oen 9012	. . . 4 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
98		ensym 9042	. . . 4 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
99	96, 97, 98	3syl 18	. . 3 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
100	7	rneqi 5951	. . . . 5 ⊢ ran 𝐴 = ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
101		dmmptg 6264	. . . . . . . 8 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐾‘𝑛)) ∈ V → dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω)
102	6	a1i 11	. . . . . . . 8 ⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ∈ V)
103	101, 102	mprg 3065	. . . . . . 7 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω
104	103, 63	eqeltri 2835	. . . . . 6 ⊢ dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
105		funmpt 6606	. . . . . 6 ⊢ Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛)))
106		funrnex 7977	. . . . . 6 ⊢ (dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V → (Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) → ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V))
107	104, 105, 106	mp2 9	. . . . 5 ⊢ ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V
108	100, 107	eqeltri 2835	. . . 4 ⊢ ran 𝐴 ∈ V
109		breq1 5151	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (𝑎 ≈ ω ↔ ran 𝐴 ≈ ω))
110		raleq 3321	. . . . . 6 ⊢ (𝑎 = ran 𝐴 → (∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
111	110	exbidv 1919	. . . . 5 ⊢ (𝑎 = ran 𝐴 → (∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
112	109, 111	imbi12d 344	. . . 4 ⊢ (𝑎 = ran 𝐴 → ((𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))))
113		ax-cc 10473	. . . 4 ⊢ (𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
114	108, 112, 113	vtocl 3558	. . 3 ⊢ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
115	95, 99, 114	mp2b 10	. 2 ⊢ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)
116	73, 115	exlimiiv 1929	1 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∃wex 1776 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 Vcvv 3478 ∅c0 4339 ifcif 4531 {csn 4631 class class class wbr 5148 ↦ cmpt 5231 × cxp 5687 dom cdm 5689 ran crn 5690 Fun wfun 6557 Fn wfn 6558 ⟶wf 6559 –1-1→wf1 6560 –1-1-onto→wf1o 6562 ‘cfv 6563 ωcom 7887 2^nd c2nd 8012 ≈ cen 8981

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-inf2 9679 ax-cc 10473

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-ral 3060 df-rex 3069 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-om 7888 df-2nd 8014 df-er 8744 df-en 8985

This theorem is referenced by: axcc2 10475

W3C validator