Metamath Proof Explorer

Theorem padct

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

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

Proof

Step Hyp Ref Expression
1 brdom2 ⊢ ( 𝐴 ≼ ω ↔ ( 𝐴 ≺ ω ∨ 𝐴 ≈ ω ) )
2 isfinite2 ⊢ ( 𝐴 ≺ ω → 𝐴 ∈ Fin )
3 isfinite4 ⊢ ( 𝐴 ∈ Fin ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
4 2 3 sylib ⊢ ( 𝐴 ≺ ω → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
5 4 adantr ⊢ ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
6 bren ⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ↔ ∃ 𝑔 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
7 5 6 sylib ⊢ ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) → ∃ 𝑔 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
8 7 3adant3 ⊢ ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) → ∃ 𝑔 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
9 f1of ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
10 9 adantl ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
11 fconstmpt ⊢ ( ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) × { 𝑍 } ) = ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 )
12 11 eqcomi ⊢ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) = ( ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) × { 𝑍 } )
13 fconst2g ⊢ ( 𝑍 ∈ 𝑉 → ( ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) : ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ⟶ { 𝑍 } ↔ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) = ( ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) × { 𝑍 } ) ) )
14 13 ad2antlr ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) : ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ⟶ { 𝑍 } ↔ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) = ( ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) × { 𝑍 } ) ) )
15 12 14 mpbiri ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) : ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ⟶ { 𝑍 } )
16 disjdif ⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∩ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) = ∅
17 16 a1i ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∩ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) = ∅ )
18 fun ⊢ ( ( ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) : ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ⟶ { 𝑍 } ) ∧ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∩ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) = ∅ ) → ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∪ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) ⟶ ( 𝐴 ∪ { 𝑍 } ) )
19 10 15 17 18 syl21anc ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∪ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) ⟶ ( 𝐴 ∪ { 𝑍 } ) )
20 fz1ssnn ⊢ ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℕ
21 undif ⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℕ ↔ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∪ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) = ℕ )
22 20 21 mpbi ⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∪ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) = ℕ
23 22 feq2i ⊢ ( ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∪ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) ⟶ ( 𝐴 ∪ { 𝑍 } ) ↔ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) )
24 19 23 sylib ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) )
25 24 3adantl3 ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) )
26 simpr ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
27 f1ofo ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –onto→ 𝐴 )
28 forn ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –onto→ 𝐴 → ran 𝑔 = 𝐴 )
29 26 27 28 3syl ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ran 𝑔 = 𝐴 )
30 ssun1 ⊢ ran 𝑔 ⊆ ( ran 𝑔 ∪ ran ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) )
31 29 30 eqsstrrdi ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → 𝐴 ⊆ ( ran 𝑔 ∪ ran ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) )
32 rnun ⊢ ran ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) = ( ran 𝑔 ∪ ran ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) )
33 31 32 sseqtrrdi ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → 𝐴 ⊆ ran ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) )
34 33 3adantl3 ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → 𝐴 ⊆ ran ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) )
35 dff1o3 ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ↔ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –onto→ 𝐴 ∧ Fun ◡ 𝑔 ) )
36 35 simprbi ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → Fun ◡ 𝑔 )
37 36 adantl ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → Fun ◡ 𝑔 )
38 cnvun ⊢ ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) = ( ◡ 𝑔 ∪ ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) )
39 38 reseq1i ⊢ ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) = ( ( ◡ 𝑔 ∪ ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 )
40 resundir ⊢ ( ( ◡ 𝑔 ∪ ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) = ( ( ◡ 𝑔 ↾ 𝐴 ) ∪ ( ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ↾ 𝐴 ) )
41 39 40 eqtri ⊢ ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) = ( ( ◡ 𝑔 ↾ 𝐴 ) ∪ ( ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ↾ 𝐴 ) )
42 dff1o4 ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ↔ ( 𝑔 Fn ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ◡ 𝑔 Fn 𝐴 ) )
43 42 simprbi ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ◡ 𝑔 Fn 𝐴 )
44 fnresdm ⊢ ( ◡ 𝑔 Fn 𝐴 → ( ◡ 𝑔 ↾ 𝐴 ) = ◡ 𝑔 )
45 43 44 syl ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( ◡ 𝑔 ↾ 𝐴 ) = ◡ 𝑔 )
46 45 adantl ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ◡ 𝑔 ↾ 𝐴 ) = ◡ 𝑔 )
47 simpl3 ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ¬ 𝑍 ∈ 𝐴 )
48 12 cnveqi ⊢ ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) = ◡ ( ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) × { 𝑍 } )
49 cnvxp ⊢ ◡ ( ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) × { 𝑍 } ) = ( { 𝑍 } × ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
50 48 49 eqtri ⊢ ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) = ( { 𝑍 } × ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
51 50 reseq1i ⊢ ( ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ↾ 𝐴 ) = ( ( { 𝑍 } × ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) ↾ 𝐴 )
52 ineqcom ⊢ ( ( { 𝑍 } ∩ 𝐴 ) = ∅ ↔ ( 𝐴 ∩ { 𝑍 } ) = ∅ )
53 disjsn ⊢ ( ( 𝐴 ∩ { 𝑍 } ) = ∅ ↔ ¬ 𝑍 ∈ 𝐴 )
54 52 53 sylbbr ⊢ ( ¬ 𝑍 ∈ 𝐴 → ( { 𝑍 } ∩ 𝐴 ) = ∅ )
55 xpdisjres ⊢ ( ( { 𝑍 } ∩ 𝐴 ) = ∅ → ( ( { 𝑍 } × ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) ↾ 𝐴 ) = ∅ )
56 54 55 syl ⊢ ( ¬ 𝑍 ∈ 𝐴 → ( ( { 𝑍 } × ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) ↾ 𝐴 ) = ∅ )
57 51 56 eqtrid ⊢ ( ¬ 𝑍 ∈ 𝐴 → ( ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ↾ 𝐴 ) = ∅ )
58 47 57 syl ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ↾ 𝐴 ) = ∅ )
59 46 58 uneq12d ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ( ◡ 𝑔 ↾ 𝐴 ) ∪ ( ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ↾ 𝐴 ) ) = ( ◡ 𝑔 ∪ ∅ ) )
60 un0 ⊢ ( ◡ 𝑔 ∪ ∅ ) = ◡ 𝑔
61 59 60 eqtrdi ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ( ◡ 𝑔 ↾ 𝐴 ) ∪ ( ◡ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ↾ 𝐴 ) ) = ◡ 𝑔 )
62 41 61 eqtrid ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) = ◡ 𝑔 )
63 62 funeqd ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( Fun ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) ↔ Fun ◡ 𝑔 ) )
64 37 63 mpbird ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → Fun ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) )
65 vex ⊢ 𝑔 ∈ V
66 nnex ⊢ ℕ ∈ V
67 66 difexi ⊢ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∈ V
68 snex ⊢ { 𝑍 } ∈ V
69 67 68 xpex ⊢ ( ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) × { 𝑍 } ) ∈ V
70 11 69 eqeltrri ⊢ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ∈ V
71 65 70 unex ⊢ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ∈ V
72 feq1 ⊢ ( 𝑓 = ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) → ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ↔ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ) )
73 rneq ⊢ ( 𝑓 = ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) → ran 𝑓 = ran ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) )
74 73 sseq2d ⊢ ( 𝑓 = ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) → ( 𝐴 ⊆ ran 𝑓 ↔ 𝐴 ⊆ ran ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ) )
75 cnveq ⊢ ( 𝑓 = ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) → ◡ 𝑓 = ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) )
76 75 reseq1d ⊢ ( 𝑓 = ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) → ( ◡ 𝑓 ↾ 𝐴 ) = ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) )
77 76 funeqd ⊢ ( 𝑓 = ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) → ( Fun ( ◡ 𝑓 ↾ 𝐴 ) ↔ Fun ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) ) )
78 72 74 77 3anbi123d ⊢ ( 𝑓 = ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) → ( ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ↔ ( ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ∧ Fun ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) ) ) )
79 71 78 spcev ⊢ ( ( ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ∧ Fun ( ◡ ( 𝑔 ∪ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ↦ 𝑍 ) ) ↾ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
80 25 34 64 79 syl3anc ⊢ ( ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) ∧ 𝑔 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
81 8 80 exlimddv ⊢ ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
82 81 3expia ⊢ ( ( 𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ) → ( ¬ 𝑍 ∈ 𝐴 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) )
83 nnenom ⊢ ℕ ≈ ω
84 ensym ⊢ ( 𝐴 ≈ ω → ω ≈ 𝐴 )
85 84 adantr ⊢ ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) → ω ≈ 𝐴 )
86 entr ⊢ ( ( ℕ ≈ ω ∧ ω ≈ 𝐴 ) → ℕ ≈ 𝐴 )
87 83 85 86 sylancr ⊢ ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) → ℕ ≈ 𝐴 )
88 bren ⊢ ( ℕ ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 )
89 87 88 sylib ⊢ ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 )
90 simpr ⊢ ( ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝑓 : ℕ –1-1-onto→ 𝐴 )
91 f1of ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → 𝑓 : ℕ ⟶ 𝐴 )
92 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑍 } )
93 fss ⊢ ( ( 𝑓 : ℕ ⟶ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∪ { 𝑍 } ) ) → 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) )
94 92 93 mpan2 ⊢ ( 𝑓 : ℕ ⟶ 𝐴 → 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) )
95 90 91 94 3syl ⊢ ( ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) )
96 f1ofo ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → 𝑓 : ℕ –onto→ 𝐴 )
97 forn ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ran 𝑓 = 𝐴 )
98 90 96 97 3syl ⊢ ( ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ran 𝑓 = 𝐴 )
99 98 eqimsscd ⊢ ( ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → 𝐴 ⊆ ran 𝑓 )
100 f1ocnv ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1-onto→ ℕ )
101 f1of1 ⊢ ( ◡ 𝑓 : 𝐴 –1-1-onto→ ℕ → ◡ 𝑓 : 𝐴 –1-1→ ℕ )
102 90 100 101 3syl ⊢ ( ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ◡ 𝑓 : 𝐴 –1-1→ ℕ )
103 ssid ⊢ 𝐴 ⊆ 𝐴
104 f1ores ⊢ ( ( ◡ 𝑓 : 𝐴 –1-1→ ℕ ∧ 𝐴 ⊆ 𝐴 ) → ( ◡ 𝑓 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( ◡ 𝑓 “ 𝐴 ) )
105 103 104 mpan2 ⊢ ( ◡ 𝑓 : 𝐴 –1-1→ ℕ → ( ◡ 𝑓 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( ◡ 𝑓 “ 𝐴 ) )
106 f1ofun ⊢ ( ( ◡ 𝑓 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( ◡ 𝑓 “ 𝐴 ) → Fun ( ◡ 𝑓 ↾ 𝐴 ) )
107 102 105 106 3syl ⊢ ( ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → Fun ( ◡ 𝑓 ↾ 𝐴 ) )
108 95 99 107 3jca ⊢ ( ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 : ℕ –1-1-onto→ 𝐴 ) → ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
109 108 ex ⊢ ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) → ( 𝑓 : ℕ –1-1-onto→ 𝐴 → ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) )
110 109 eximdv ⊢ ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) → ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐴 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) )
111 89 110 mpd ⊢ ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
112 111 a1d ⊢ ( ( 𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉 ) → ( ¬ 𝑍 ∈ 𝐴 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) )
113 82 112 jaoian ⊢ ( ( ( 𝐴 ≺ ω ∨ 𝐴 ≈ ω ) ∧ 𝑍 ∈ 𝑉 ) → ( ¬ 𝑍 ∈ 𝐴 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) )
114 113 3impia ⊢ ( ( ( 𝐴 ≺ ω ∨ 𝐴 ≈ ω ) ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
115 1 114 syl3an1b ⊢ ( ( 𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { 𝑍 } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )