Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  padct Structured version   Visualization version   GIF version

Theorem padct 29837
Description: Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.)
Assertion
Ref Expression
padct ((𝐴 ≼ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
Distinct variable groups:   𝐴,𝑓   𝑓,𝑉   𝑓,𝑍

Proof of Theorem padct
Dummy variables 𝑔 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdom2 8143 . 2 (𝐴 ≼ ω ↔ (𝐴 ≺ ω ∨ 𝐴 ≈ ω))
2 isfinite2 8378 . . . . . . . . . 10 (𝐴 ≺ ω → 𝐴 ∈ Fin)
3 isfinite4 13355 . . . . . . . . . 10 (𝐴 ∈ Fin ↔ (1...(♯‘𝐴)) ≈ 𝐴)
42, 3sylib 208 . . . . . . . . 9 (𝐴 ≺ ω → (1...(♯‘𝐴)) ≈ 𝐴)
54adantr 466 . . . . . . . 8 ((𝐴 ≺ ω ∧ 𝑍𝑉) → (1...(♯‘𝐴)) ≈ 𝐴)
6 bren 8122 . . . . . . . 8 ((1...(♯‘𝐴)) ≈ 𝐴 ↔ ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴)
75, 6sylib 208 . . . . . . 7 ((𝐴 ≺ ω ∧ 𝑍𝑉) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴)
873adant3 1126 . . . . . 6 ((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴)
9 nfv 1995 . . . . . . 7 𝑔(𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴)
10 nfv 1995 . . . . . . 7 𝑔𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))
11 f1of 6279 . . . . . . . . . . . . 13 (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴𝑔:(1...(♯‘𝐴))⟶𝐴)
1211adantl 467 . . . . . . . . . . . 12 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → 𝑔:(1...(♯‘𝐴))⟶𝐴)
13 fconstmpt 5302 . . . . . . . . . . . . . 14 ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) = (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)
1413eqcomi 2780 . . . . . . . . . . . . 13 (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})
15 simplr 752 . . . . . . . . . . . . . 14 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → 𝑍𝑉)
16 fconst2g 6615 . . . . . . . . . . . . . 14 (𝑍𝑉 → ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})))
1715, 16syl 17 . . . . . . . . . . . . 13 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})))
1814, 17mpbiri 248 . . . . . . . . . . . 12 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍})
19 disjdif 4183 . . . . . . . . . . . . 13 ((1...(♯‘𝐴)) ∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅
2019a1i 11 . . . . . . . . . . . 12 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ((1...(♯‘𝐴)) ∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅)
21 fun 6207 . . . . . . . . . . . 12 (((𝑔:(1...(♯‘𝐴))⟶𝐴 ∧ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(♯‘𝐴)))⟶{𝑍}) ∧ ((1...(♯‘𝐴)) ∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}))
2212, 18, 20, 21syl21anc 1475 . . . . . . . . . . 11 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}))
23 fz1ssnn 12579 . . . . . . . . . . . . 13 (1...(♯‘𝐴)) ⊆ ℕ
24 undif 4192 . . . . . . . . . . . . 13 ((1...(♯‘𝐴)) ⊆ ℕ ↔ ((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴)))) = ℕ)
2523, 24mpbi 220 . . . . . . . . . . . 12 ((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴)))) = ℕ
2625feq2i 6176 . . . . . . . . . . 11 ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖ (1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))
2722, 26sylib 208 . . . . . . . . . 10 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))
28273adantl3 1173 . . . . . . . . 9 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))
29 ssid 3773 . . . . . . . . . . . . . 14 𝐴𝐴
30 simpr 471 . . . . . . . . . . . . . . 15 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴)
31 f1ofo 6286 . . . . . . . . . . . . . . 15 (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴𝑔:(1...(♯‘𝐴))–onto𝐴)
32 forn 6260 . . . . . . . . . . . . . . 15 (𝑔:(1...(♯‘𝐴))–onto𝐴 → ran 𝑔 = 𝐴)
3330, 31, 323syl 18 . . . . . . . . . . . . . 14 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ran 𝑔 = 𝐴)
3429, 33syl5sseqr 3803 . . . . . . . . . . . . 13 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → 𝐴 ⊆ ran 𝑔)
3534orcd 862 . . . . . . . . . . . 12 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝐴 ⊆ ran 𝑔𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
36 ssun 3943 . . . . . . . . . . . 12 ((𝐴 ⊆ ran 𝑔𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
3735, 36syl 17 . . . . . . . . . . 11 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
38 rnun 5681 . . . . . . . . . . 11 ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) = (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍))
3937, 38syl6sseqr 3801 . . . . . . . . . 10 (((𝐴 ≺ ω ∧ 𝑍𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
40393adantl3 1173 . . . . . . . . 9 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
41 dff1o3 6285 . . . . . . . . . . . 12 (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴 ↔ (𝑔:(1...(♯‘𝐴))–onto𝐴 ∧ Fun 𝑔))
4241simprbi 484 . . . . . . . . . . 11 (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴 → Fun 𝑔)
4342adantl 467 . . . . . . . . . 10 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → Fun 𝑔)
44 cnvun 5678 . . . . . . . . . . . . . 14 (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) = (𝑔(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍))
4544reseq1i 5529 . . . . . . . . . . . . 13 ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((𝑔(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴)
46 resundir 5551 . . . . . . . . . . . . 13 ((𝑔(𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((𝑔𝐴) ∪ ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴))
4745, 46eqtri 2793 . . . . . . . . . . . 12 ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((𝑔𝐴) ∪ ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴))
48 dff1o4 6287 . . . . . . . . . . . . . . . . 17 (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴 ↔ (𝑔 Fn (1...(♯‘𝐴)) ∧ 𝑔 Fn 𝐴))
4948simprbi 484 . . . . . . . . . . . . . . . 16 (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴𝑔 Fn 𝐴)
50 fnresdm 6139 . . . . . . . . . . . . . . . 16 (𝑔 Fn 𝐴 → (𝑔𝐴) = 𝑔)
5149, 50syl 17 . . . . . . . . . . . . . . 15 (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴 → (𝑔𝐴) = 𝑔)
5251adantl 467 . . . . . . . . . . . . . 14 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → (𝑔𝐴) = 𝑔)
53 simpl3 1231 . . . . . . . . . . . . . . 15 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ¬ 𝑍𝐴)
5414cnveqi 5434 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍})
55 cnvxp 5691 . . . . . . . . . . . . . . . . . 18 ((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) = ({𝑍} × (ℕ ∖ (1...(♯‘𝐴))))
5654, 55eqtri 2793 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) = ({𝑍} × (ℕ ∖ (1...(♯‘𝐴))))
5756reseq1i 5529 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴) = (({𝑍} × (ℕ ∖ (1...(♯‘𝐴)))) ↾ 𝐴)
58 incom 3956 . . . . . . . . . . . . . . . . . 18 (𝐴 ∩ {𝑍}) = ({𝑍} ∩ 𝐴)
59 disjsn 4384 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍𝐴)
6059biimpri 218 . . . . . . . . . . . . . . . . . 18 𝑍𝐴 → (𝐴 ∩ {𝑍}) = ∅)
6158, 60syl5eqr 2819 . . . . . . . . . . . . . . . . 17 𝑍𝐴 → ({𝑍} ∩ 𝐴) = ∅)
62 xpdisjres 29749 . . . . . . . . . . . . . . . . 17 (({𝑍} ∩ 𝐴) = ∅ → (({𝑍} × (ℕ ∖ (1...(♯‘𝐴)))) ↾ 𝐴) = ∅)
6361, 62syl 17 . . . . . . . . . . . . . . . 16 𝑍𝐴 → (({𝑍} × (ℕ ∖ (1...(♯‘𝐴)))) ↾ 𝐴) = ∅)
6457, 63syl5eq 2817 . . . . . . . . . . . . . . 15 𝑍𝐴 → ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴) = ∅)
6553, 64syl 17 . . . . . . . . . . . . . 14 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴) = ∅)
6652, 65uneq12d 3919 . . . . . . . . . . . . 13 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ((𝑔𝐴) ∪ ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴)) = (𝑔 ∪ ∅))
67 un0 4112 . . . . . . . . . . . . 13 (𝑔 ∪ ∅) = 𝑔
6866, 67syl6eq 2821 . . . . . . . . . . . 12 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ((𝑔𝐴) ∪ ((𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ↾ 𝐴)) = 𝑔)
6947, 68syl5eq 2817 . . . . . . . . . . 11 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = 𝑔)
7069funeqd 6052 . . . . . . . . . 10 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → (Fun ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴) ↔ Fun 𝑔))
7143, 70mpbird 247 . . . . . . . . 9 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → Fun ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴))
72 vex 3354 . . . . . . . . . . 11 𝑔 ∈ V
73 nnex 11232 . . . . . . . . . . . . 13 ℕ ∈ V
74 difexg 4943 . . . . . . . . . . . . 13 (ℕ ∈ V → (ℕ ∖ (1...(♯‘𝐴))) ∈ V)
7573, 74ax-mp 5 . . . . . . . . . . . 12 (ℕ ∖ (1...(♯‘𝐴))) ∈ V
7675mptex 6633 . . . . . . . . . . 11 (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍) ∈ V
7772, 76unex 7107 . . . . . . . . . 10 (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ∈ V
78 feq1 6165 . . . . . . . . . . 11 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})))
79 rneq 5488 . . . . . . . . . . . 12 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → ran 𝑓 = ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
8079sseq2d 3782 . . . . . . . . . . 11 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (𝐴 ⊆ ran 𝑓𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍))))
81 cnveq 5433 . . . . . . . . . . . . 13 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → 𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)))
82 eqidd 2772 . . . . . . . . . . . . 13 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → 𝐴 = 𝐴)
8381, 82reseq12d 5534 . . . . . . . . . . . 12 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (𝑓𝐴) = ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴))
8483funeqd 6052 . . . . . . . . . . 11 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → (Fun (𝑓𝐴) ↔ Fun ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴)))
8578, 80, 843anbi123d 1547 . . . . . . . . . 10 (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) → ((𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)) ↔ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ∧ Fun ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴))))
8677, 85spcev 3451 . . . . . . . . 9 (((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ∧ Fun ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(♯‘𝐴))) ↦ 𝑍)) ↾ 𝐴)) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
8728, 40, 71, 86syl3anc 1476 . . . . . . . 8 (((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
8887ex 397 . . . . . . 7 ((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) → (𝑔:(1...(♯‘𝐴))–1-1-onto𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))))
899, 10, 88exlimd 2243 . . . . . 6 ((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) → (∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))))
908, 89mpd 15 . . . . 5 ((𝐴 ≺ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
91903expia 1114 . . . 4 ((𝐴 ≺ ω ∧ 𝑍𝑉) → (¬ 𝑍𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))))
92 nnenom 12987 . . . . . . . 8 ℕ ≈ ω
93 simpl 468 . . . . . . . . 9 ((𝐴 ≈ ω ∧ 𝑍𝑉) → 𝐴 ≈ ω)
9493ensymd 8164 . . . . . . . 8 ((𝐴 ≈ ω ∧ 𝑍𝑉) → ω ≈ 𝐴)
95 entr 8165 . . . . . . . 8 ((ℕ ≈ ω ∧ ω ≈ 𝐴) → ℕ ≈ 𝐴)
9692, 94, 95sylancr 575 . . . . . . 7 ((𝐴 ≈ ω ∧ 𝑍𝑉) → ℕ ≈ 𝐴)
97 bren 8122 . . . . . . 7 (ℕ ≈ 𝐴 ↔ ∃𝑓 𝑓:ℕ–1-1-onto𝐴)
9896, 97sylib 208 . . . . . 6 ((𝐴 ≈ ω ∧ 𝑍𝑉) → ∃𝑓 𝑓:ℕ–1-1-onto𝐴)
99 nfv 1995 . . . . . . 7 𝑓(𝐴 ≈ ω ∧ 𝑍𝑉)
100 simpr 471 . . . . . . . . . 10 (((𝐴 ≈ ω ∧ 𝑍𝑉) ∧ 𝑓:ℕ–1-1-onto𝐴) → 𝑓:ℕ–1-1-onto𝐴)
101 f1of 6279 . . . . . . . . . 10 (𝑓:ℕ–1-1-onto𝐴𝑓:ℕ⟶𝐴)
102 ssun1 3927 . . . . . . . . . . 11 𝐴 ⊆ (𝐴 ∪ {𝑍})
103 fss 6197 . . . . . . . . . . 11 ((𝑓:ℕ⟶𝐴𝐴 ⊆ (𝐴 ∪ {𝑍})) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍}))
104102, 103mpan2 671 . . . . . . . . . 10 (𝑓:ℕ⟶𝐴𝑓:ℕ⟶(𝐴 ∪ {𝑍}))
105100, 101, 1043syl 18 . . . . . . . . 9 (((𝐴 ≈ ω ∧ 𝑍𝑉) ∧ 𝑓:ℕ–1-1-onto𝐴) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍}))
106 f1ofo 6286 . . . . . . . . . . 11 (𝑓:ℕ–1-1-onto𝐴𝑓:ℕ–onto𝐴)
107 forn 6260 . . . . . . . . . . 11 (𝑓:ℕ–onto𝐴 → ran 𝑓 = 𝐴)
108100, 106, 1073syl 18 . . . . . . . . . 10 (((𝐴 ≈ ω ∧ 𝑍𝑉) ∧ 𝑓:ℕ–1-1-onto𝐴) → ran 𝑓 = 𝐴)
10929, 108syl5sseqr 3803 . . . . . . . . 9 (((𝐴 ≈ ω ∧ 𝑍𝑉) ∧ 𝑓:ℕ–1-1-onto𝐴) → 𝐴 ⊆ ran 𝑓)
110 f1ocnv 6291 . . . . . . . . . . 11 (𝑓:ℕ–1-1-onto𝐴𝑓:𝐴1-1-onto→ℕ)
111 f1of1 6278 . . . . . . . . . . 11 (𝑓:𝐴1-1-onto→ℕ → 𝑓:𝐴1-1→ℕ)
112100, 110, 1113syl 18 . . . . . . . . . 10 (((𝐴 ≈ ω ∧ 𝑍𝑉) ∧ 𝑓:ℕ–1-1-onto𝐴) → 𝑓:𝐴1-1→ℕ)
113 f1ores 6293 . . . . . . . . . . 11 ((𝑓:𝐴1-1→ℕ ∧ 𝐴𝐴) → (𝑓𝐴):𝐴1-1-onto→(𝑓𝐴))
11429, 113mpan2 671 . . . . . . . . . 10 (𝑓:𝐴1-1→ℕ → (𝑓𝐴):𝐴1-1-onto→(𝑓𝐴))
115 f1ofun 6281 . . . . . . . . . 10 ((𝑓𝐴):𝐴1-1-onto→(𝑓𝐴) → Fun (𝑓𝐴))
116112, 114, 1153syl 18 . . . . . . . . 9 (((𝐴 ≈ ω ∧ 𝑍𝑉) ∧ 𝑓:ℕ–1-1-onto𝐴) → Fun (𝑓𝐴))
117105, 109, 1163jca 1122 . . . . . . . 8 (((𝐴 ≈ ω ∧ 𝑍𝑉) ∧ 𝑓:ℕ–1-1-onto𝐴) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
118117ex 397 . . . . . . 7 ((𝐴 ≈ ω ∧ 𝑍𝑉) → (𝑓:ℕ–1-1-onto𝐴 → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))))
11999, 118eximd 2241 . . . . . 6 ((𝐴 ≈ ω ∧ 𝑍𝑉) → (∃𝑓 𝑓:ℕ–1-1-onto𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))))
12098, 119mpd 15 . . . . 5 ((𝐴 ≈ ω ∧ 𝑍𝑉) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
121120a1d 25 . . . 4 ((𝐴 ≈ ω ∧ 𝑍𝑉) → (¬ 𝑍𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))))
12291, 121jaoian 941 . . 3 (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍𝑉) → (¬ 𝑍𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))))
1231223impia 1109 . 2 (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
1241, 123syl3an1b 1509 1 ((𝐴 ≼ ω ∧ 𝑍𝑉 ∧ ¬ 𝑍𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 836  w3a 1071   = wceq 1631  wex 1852  wcel 2145  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  {csn 4317   class class class wbr 4787  cmpt 4864   × cxp 5248  ccnv 5249  ran crn 5251  cres 5252  cima 5253  Fun wfun 6024   Fn wfn 6025  wf 6026  1-1wf1 6027  ontowfo 6028  1-1-ontowf1o 6029  cfv 6030  (class class class)co 6796  ωcom 7216  cen 8110  cdom 8111  csdm 8112  Fincfn 8113  1c1 10143  cn 11226  ...cfz 12533  chash 13321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100  ax-inf2 8706  ax-cnex 10198  ax-resscn 10199  ax-1cn 10200  ax-icn 10201  ax-addcl 10202  ax-addrcl 10203  ax-mulcl 10204  ax-mulrcl 10205  ax-mulcom 10206  ax-addass 10207  ax-mulass 10208  ax-distr 10209  ax-i2m1 10210  ax-1ne0 10211  ax-1rid 10212  ax-rnegex 10213  ax-rrecex 10214  ax-cnre 10215  ax-pre-lttri 10216  ax-pre-lttrn 10217  ax-pre-ltadd 10218  ax-pre-mulgt0 10219
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6757  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-om 7217  df-1st 7319  df-2nd 7320  df-wrecs 7563  df-recs 7625  df-rdg 7663  df-1o 7717  df-er 7900  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-card 8969  df-pnf 10282  df-mnf 10283  df-xr 10284  df-ltxr 10285  df-le 10286  df-sub 10474  df-neg 10475  df-nn 11227  df-n0 11500  df-z 11585  df-uz 11894  df-fz 12534  df-hash 13322
This theorem is referenced by:  carsggect  30720
  Copyright terms: Public domain W3C validator