Theorem padct 32809

Description: Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.) Avoid ax-rep 5213. (Revised by GG, 2-Apr-2026.)

Assertion

Ref	Expression
padct	⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))

Distinct variable groups:   𝐴,𝑓   𝑓,𝑉   𝑓,𝑍

Proof of Theorem padct

Dummy variables 𝑔 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brdom2 8923	. 2 ⊢ (𝐴 ≼ ω ↔ (𝐴 ≺ ω ∨ 𝐴 ≈ ω))
2		isfinite2 9202	. . . . . . . . . 10 ⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
3		isfinite4 14318	. . . . . . . . . 10 ⊢ (𝐴 ∈ Fin ↔ (1...(♯‘𝐴)) ≈ 𝐴)
4	2, 3	sylib 218	. . . . . . . . 9 ⊢ (𝐴 ≺ ω → (1...(♯‘𝐴)) ≈ 𝐴)
5	4	adantr 480	. . . . . . . 8 ⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (1...(♯‘𝐴)) ≈ 𝐴)
6		bren 8897	. . . . . . . 8 ⊢ ((1...(♯‘𝐴)) ≈ 𝐴 ↔ ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴)
7	5, 6	sylib 218	. . . . . . 7 ⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴)
8	7	3adant3 1133	. . . . . 6 ⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴)
9		f1of 6775	. . . . . . . . . . 11 ⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(♯‘𝐴))⟶𝐴)
10	9	adantl 481	. . . . . . . . . 10 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(♯‘𝐴))⟶𝐴)
11		fconstmpt 5687	. . . . . . . . . . . 12 ⊢ ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) = (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)
12	11	eqcomi 2746	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})
13		fconst2g 7152	. . . . . . . . . . . 12 ⊢ (𝑍 ∈ 𝑉 → ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})))
14	13	ad2antlr 728	. . . . . . . . . . 11 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})))
15	12, 14	mpbiri 258	. . . . . . . . . 10 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍})
16		disjdif 4413	. . . . . . . . . . 11 ⊢ ((1...(♯‘𝐴)) ∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅
17	16	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((1...(♯‘𝐴)) ∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅)
18		fun 6697	. . . . . . . . . 10 ⊢ (((𝑔:(1...(♯‘𝐴))⟶𝐴 ∧ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍}) ∧ ((1...(♯‘𝐴)) ∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}))
19	10, 15, 17, 18	syl21anc 838	. . . . . . . . 9 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}))
20		fz1ssnn 13503	. . . . . . . . . . 11 ⊢ (1...(♯‘𝐴)) ⊆ ℕ
21		undif 4423	. . . . . . . . . . 11 ⊢ ((1...(♯‘𝐴)) ⊆ ℕ ↔ ((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴)))) = ℕ)
22	20, 21	mpbi 230	. . . . . . . . . 10 ⊢ ((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴)))) = ℕ
23	22	feq2i 6655	. . . . . . . . 9 ⊢ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))
24	19, 23	sylib 218	. . . . . . . 8 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))
25	24	3adantl3 1170	. . . . . . 7 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))
26		simpr 484	. . . . . . . . . . 11 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴)
27		f1ofo 6782	. . . . . . . . . . 11 ⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(♯‘𝐴))–onto→𝐴)
28		forn 6750	. . . . . . . . . . 11 ⊢ (𝑔:(1...(♯‘𝐴))–onto→𝐴 → ran 𝑔 = 𝐴)
29	26, 27, 28	3syl 18	. . . . . . . . . 10 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ran 𝑔 = 𝐴)
30		ssun1 4119	. . . . . . . . . 10 ⊢ ran 𝑔 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍))
31	29, 30	eqsstrrdi 3968	. . . . . . . . 9 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
32		rnun 6104	. . . . . . . . 9 ⊢ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) = (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍))
33	31, 32	sseqtrrdi 3964	. . . . . . . 8 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
34	33	3adantl3 1170	. . . . . . 7 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
35		dff1o3 6781	. . . . . . . . . 10 ⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 ↔ (𝑔:(1...(♯‘𝐴))–onto→𝐴 ∧ Fun ◡𝑔))
36	35	simprbi 497	. . . . . . . . 9 ⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → Fun ◡𝑔)
37	36	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → Fun ◡𝑔)
38		cnvun 6101	. . . . . . . . . . . 12 ⊢ ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) = (◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍))
39	38	reseq1i 5935	. . . . . . . . . . 11 ⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴)
40		resundir 5954	. . . . . . . . . . 11 ⊢ ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴))
41	39, 40	eqtri 2760	. . . . . . . . . 10 ⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴))
42		dff1o4 6783	. . . . . . . . . . . . . . 15 ⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 ↔ (𝑔 Fn (1...(♯‘𝐴)) ∧ ◡𝑔 Fn 𝐴))
43	42	simprbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → ◡𝑔 Fn 𝐴)
44		fnresdm 6612	. . . . . . . . . . . . . 14 ⊢ (◡𝑔 Fn 𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔)
45	43, 44	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔)
46	45	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡𝑔 ↾ 𝐴) = ◡𝑔)
47		simpl3 1195	. . . . . . . . . . . . 13 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ¬ 𝑍 ∈ 𝐴)
48	12	cnveqi 5824	. . . . . . . . . . . . . . . 16 ⊢ ◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ◡((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})
49		cnvxp 6116	. . . . . . . . . . . . . . . 16 ⊢ ◡((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) = ({𝑍} × (ℕ ∖ (1...(♯‘𝐴))))
50	48, 49	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ ◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ({𝑍} × (ℕ ∖ (1...(♯‘𝐴))))
51	50	reseq1i 5935	. . . . . . . . . . . . . 14 ⊢ (◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴) = (({𝑍} × (ℕ ∖ (1...(♯‘𝐴)))) ↾ 𝐴)
52		ineqcom 4151	. . . . . . . . . . . . . . . 16 ⊢ (({𝑍} ∩ 𝐴) = ∅ ↔ (𝐴 ∩ {𝑍}) = ∅)
53		disjsn 4656	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ 𝐴)
54	52, 53	sylbbr 236	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑍 ∈ 𝐴 → ({𝑍} ∩ 𝐴) = ∅)
55		xpdisjres 32686	. . . . . . . . . . . . . . 15 ⊢ (({𝑍} ∩ 𝐴) = ∅ → (({𝑍} × (ℕ ∖ (1...(♯‘𝐴)))) ↾ 𝐴) = ∅)
56	54, 55	syl 17	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑍 ∈ 𝐴 → (({𝑍} × (ℕ ∖ (1...(♯‘𝐴)))) ↾ 𝐴) = ∅)
57	51, 56	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ (¬ 𝑍 ∈ 𝐴 → (◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴) = ∅)
58	47, 57	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴) = ∅)
59	46, 58	uneq12d 4110	. . . . . . . . . . 11 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴)) = (◡𝑔 ∪ ∅))
60		un0 4335	. . . . . . . . . . 11 ⊢ (◡𝑔 ∪ ∅) = ◡𝑔
61	59, 60	eqtrdi 2788	. . . . . . . . . 10 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴)) = ◡𝑔)
62	41, 61	eqtrid 2784	. . . . . . . . 9 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ◡𝑔)
63	62	funeqd 6515	. . . . . . . 8 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) ↔ Fun ◡𝑔))
64	37, 63	mpbird 257	. . . . . . 7 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴))
65		vex 3434	. . . . . . . . 9 ⊢ 𝑔 ∈ V
66		nnex 12174	. . . . . . . . . . . 12 ⊢ ℕ ∈ V
67	66	difexi 5268	. . . . . . . . . . 11 ⊢ (ℕ ∖ (1...(♯‘𝐴))) ∈ V
68		snex 5377	. . . . . . . . . . 11 ⊢ {𝑍} ∈ V
69	67, 68	xpex 7701	. . . . . . . . . 10 ⊢ ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) ∈ V
70	11, 69	eqeltrri 2834	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ∈ V
71	65, 70	unex 7692	. . . . . . . 8 ⊢ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ∈ V
72		feq1 6641	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})))
73		rneq 5886	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → ran 𝑓 = ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
74	73	sseq2d 3955	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (𝐴 ⊆ ran 𝑓 ↔ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍))))
75		cnveq 5823	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → ◡𝑓 = ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
76	75	reseq1d 5938	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (◡𝑓 ↾ 𝐴) = (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴))
77	76	funeqd 6515	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (Fun (◡𝑓 ↾ 𝐴) ↔ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴)))
78	72, 74, 77	3anbi123d 1439	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → ((𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) ↔ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ∧ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴))))
79	71, 78	spcev 3549	. . . . . . 7 ⊢ (((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ∧ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴)) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
80	25, 34, 64, 79	syl3anc 1374	. . . . . 6 ⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
81	8, 80	exlimddv 1937	. . . . 5 ⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
82	81	3expia 1122	. . . 4 ⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))))
83		nnenom 13936	. . . . . . . 8 ⊢ ℕ ≈ ω
84		ensym 8944	. . . . . . . . 9 ⊢ (𝐴 ≈ ω → ω ≈ 𝐴)
85	84	adantr 480	. . . . . . . 8 ⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ω ≈ 𝐴)
86		entr 8947	. . . . . . . 8 ⊢ ((ℕ ≈ ω ∧ ω ≈ 𝐴) → ℕ ≈ 𝐴)
87	83, 85, 86	sylancr 588	. . . . . . 7 ⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ℕ ≈ 𝐴)
88		bren 8897	. . . . . . 7 ⊢ (ℕ ≈ 𝐴 ↔ ∃𝑓 𝑓:ℕ–1-1-onto→𝐴)
89	87, 88	sylib 218	. . . . . 6 ⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑓 𝑓:ℕ–1-1-onto→𝐴)
90		simpr 484	. . . . . . . . . 10 ⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ–1-1-onto→𝐴)
91		f1of 6775	. . . . . . . . . 10 ⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ⟶𝐴)
92		ssun1 4119	. . . . . . . . . . 11 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝑍})
93		fss 6679	. . . . . . . . . . 11 ⊢ ((𝑓:ℕ⟶𝐴 ∧ 𝐴 ⊆ (𝐴 ∪ {𝑍})) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍}))
94	92, 93	mpan2 692	. . . . . . . . . 10 ⊢ (𝑓:ℕ⟶𝐴 → 𝑓:ℕ⟶(𝐴 ∪ {𝑍}))
95	90, 91, 94	3syl 18	. . . . . . . . 9 ⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍}))
96		f1ofo 6782	. . . . . . . . . . 11 ⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ–onto→𝐴)
97		forn 6750	. . . . . . . . . . 11 ⊢ (𝑓:ℕ–onto→𝐴 → ran 𝑓 = 𝐴)
98	90, 96, 97	3syl 18	. . . . . . . . . 10 ⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran 𝑓 = 𝐴)
99	98	eqimsscd 3980	. . . . . . . . 9 ⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝐴 ⊆ ran 𝑓)
100		f1ocnv 6787	. . . . . . . . . . 11 ⊢ (𝑓:ℕ–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→ℕ)
101		f1of1 6774	. . . . . . . . . . 11 ⊢ (◡𝑓:𝐴–1-1-onto→ℕ → ◡𝑓:𝐴–1-1→ℕ)
102	90, 100, 101	3syl 18	. . . . . . . . . 10 ⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ◡𝑓:𝐴–1-1→ℕ)
103		ssid 3945	. . . . . . . . . . 11 ⊢ 𝐴 ⊆ 𝐴
104		f1ores 6789	. . . . . . . . . . 11 ⊢ ((◡𝑓:𝐴–1-1→ℕ ∧ 𝐴 ⊆ 𝐴) → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴))
105	103, 104	mpan2 692	. . . . . . . . . 10 ⊢ (◡𝑓:𝐴–1-1→ℕ → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴))
106		f1ofun 6777	. . . . . . . . . 10 ⊢ ((◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴) → Fun (◡𝑓 ↾ 𝐴))
107	102, 105, 106	3syl 18	. . . . . . . . 9 ⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → Fun (◡𝑓 ↾ 𝐴))
108	95, 99, 107	3jca 1129	. . . . . . . 8 ⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
109	108	ex 412	. . . . . . 7 ⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))))
110	109	eximdv 1919	. . . . . 6 ⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (∃𝑓 𝑓:ℕ–1-1-onto→𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))))
111	89, 110	mpd 15	. . . . 5 ⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
112	111	a1d 25	. . . 4 ⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))))
113	82, 112	jaoian 959	. . 3 ⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))))
114	113	3impia 1118	. 2 ⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
115	1, 114	syl3an1b 1406	1 ⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889   ⊆ wss 3890  ∅c0 4274  {csn 4568   class class class wbr 5086   ↦ cmpt 5167   × cxp 5623  ^◡ccnv 5624  ran crn 5626   ↾ cres 5627   “ cima 5628  Fun wfun 6487   Fn wfn 6488  ⟶wf 6489  –1-1→wf1 6490  –onto→wfo 6491  –1-1-onto→wf1o 6492  ‘cfv 6493  (class class class)co 7361  ωcom 7811   ≈ cen 8884   ≼ cdom 8885   ≺ csdm 8886  Fincfn 8887  1c1 11033  ℕcn 12168  ...cfz 13455  ♯chash 14286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-inf2 9556  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  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-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519  df-uz 12783  df-fz 13456  df-hash 14287

This theorem is referenced by:  carsggect  34481