Metamath Proof Explorer

Theorem padct

Description: Index a countable set with integers and pad with Z . (Contributed by Thierry Arnoux, 1-Jun-2020)

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

Proof

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