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	$⊢ (A ≼ ω \land Z \in V \land \neg Z \in A) \to \exists f (f : ℕ ⟶ A \cup \{Z\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))$

Proof

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

Metamath Proof Explorer

Theorem padct

Proof