padct

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

		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		nfv	$⊢ Ⅎ g (A ≺ ω \land Z \in V \land \neg Z \in A)$
3		nfv	$⊢ Ⅎ g \exists f (f : ℕ ⟶ A \cup \{Z\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))$
4		isfinite2	$⊢ A ≺ ω \to A \in Fin$
5		isfinite4	$⊢ A \in Fin \leftrightarrow (1 \dots \|A\|) \approx A$
6	4 5	sylib	$⊢ A ≺ ω \to (1 \dots \|A\|) \approx A$
7	6	adantr	$⊢ (A ≺ ω \land Z \in V) \to (1 \dots \|A\|) \approx A$
8		bren	$⊢ (1 \dots \|A\|) \approx A \leftrightarrow \exists g g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
9	7 8	sylib	$⊢ (A ≺ ω \land Z \in V) \to \exists g g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
10	9	3adant3	$⊢ (A ≺ ω \land Z \in V \land \neg Z \in A) \to \exists g g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
11		f1of	$⊢ g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to g : (1 \dots \|A\|) ⟶ A$
12	11	adantl	$⊢ ((A ≺ ω \land Z \in V) \land g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to g : (1 \dots \|A\|) ⟶ A$
13		fconstmpt	$⊢ (ℕ ∖ (1 \dots \|A\|)) \times \{Z\} = (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)$
14	13	eqcomi	$⊢ (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z) = (ℕ ∖ (1 \dots \|A\|)) \times \{Z\}$
15		simplr	$⊢ ((A ≺ ω \land Z \in V) \land g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to Z \in V$
16		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\})$
17	15 16	syl	$⊢ ((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\})$
18	14 17	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\}$
19		disjdif	$⊢ (1 \dots \|A\|) \cap (ℕ ∖ (1 \dots \|A\|)) = \emptyset$
20	19	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$
21		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\}$
22	12 18 20 21	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\}$
23		fz1ssnn	$⊢ (1 \dots \|A\|) \subseteq ℕ$
24		undif	$⊢ (1 \dots \|A\|) \subseteq ℕ \leftrightarrow (1 \dots \|A\|) \cup (ℕ ∖ (1 \dots \|A\|)) = ℕ$
25	23 24	mpbi	$⊢ (1 \dots \|A\|) \cup (ℕ ∖ (1 \dots \|A\|)) = ℕ$
26	25	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\}$
27	22 26	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\}$
28	27	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\}$
29		ssid	$⊢ A \subseteq A$
30		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$
31		f1ofo	$⊢ g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to g : (1 \dots \|A\|) \underset{onto}{⟶} A$
32		forn	$⊢ g : (1 \dots \|A\|) \underset{onto}{⟶} A \to ran g = A$
33	30 31 32	3syl	$⊢ ((A ≺ ω \land Z \in V) \land g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to ran g = A$
34	29 33	sseqtrrid	$⊢ ((A ≺ ω \land Z \in V) \land g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to A \subseteq ran g$
35	34	orcd	$⊢ ((A ≺ ω \land Z \in V) \land g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to (A \subseteq ran g \lor A \subseteq ran (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z))$
36		ssun	$⊢ (A \subseteq ran g \lor A \subseteq ran (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)) \to A \subseteq ran g \cup ran (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)$
37	35 36	syl	$⊢ ((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)$
38		rnun	$⊢ ran (g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)) = ran g \cup ran (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)$
39	37 38	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))$
40	39	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))$
41		dff1o3	$⊢ g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \leftrightarrow (g : (1 \dots \|A\|) \underset{onto}{⟶} A \land Fun g^{-1})$
42	41	simprbi	$⊢ g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to Fun g^{-1}$
43	42	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}$
44		cnvun	$⊢ {(g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z))}^{-1} = g^{-1} \cup {(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1}$
45	44	reseq1i	$⊢ {{(g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z))}^{-1} ↾}_{A} = {(g^{-1} \cup {(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1}) ↾}_{A}$
46		resundir	$⊢ {(g^{-1} \cup {(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1}) ↾}_{A} = ({g^{-1} ↾}_{A}) \cup ({{(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1} ↾}_{A})$
47	45 46	eqtri	$⊢ {{(g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z))}^{-1} ↾}_{A} = ({g^{-1} ↾}_{A}) \cup ({{(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1} ↾}_{A})$
48		dff1o4	$⊢ g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \leftrightarrow (g Fn (1 \dots \|A\|) \land g^{-1} Fn A)$
49	48	simprbi	$⊢ g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to g^{-1} Fn A$
50		fnresdm	$⊢ g^{-1} Fn A \to {g^{-1} ↾}_{A} = g^{-1}$
51	49 50	syl	$⊢ g : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to {g^{-1} ↾}_{A} = g^{-1}$
52	51	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}$
53		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$
54	14	cnveqi	$⊢ {(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1} = {((ℕ ∖ (1 \dots \|A\|)) \times \{Z\})}^{-1}$
55		cnvxp	$⊢ {((ℕ ∖ (1 \dots \|A\|)) \times \{Z\})}^{-1} = \{Z\} \times (ℕ ∖ (1 \dots \|A\|))$
56	54 55	eqtri	$⊢ {(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1} = \{Z\} \times (ℕ ∖ (1 \dots \|A\|))$
57	56	reseq1i	$⊢ {{(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1} ↾}_{A} = {(\{Z\} \times (ℕ ∖ (1 \dots \|A\|))) ↾}_{A}$
58		incom	$⊢ A \cap \{Z\} = \{Z\} \cap A$
59		disjsn	$⊢ A \cap \{Z\} = \emptyset \leftrightarrow \neg Z \in A$
60	59	biimpri	$⊢ \neg Z \in A \to A \cap \{Z\} = \emptyset$
61	58 60	eqtr3id	$⊢ \neg Z \in A \to \{Z\} \cap A = \emptyset$
62		xpdisjres	$⊢ \{Z\} \cap A = \emptyset \to {(\{Z\} \times (ℕ ∖ (1 \dots \|A\|))) ↾}_{A} = \emptyset$
63	61 62	syl	$⊢ \neg Z \in A \to {(\{Z\} \times (ℕ ∖ (1 \dots \|A\|))) ↾}_{A} = \emptyset$
64	57 63	eqtrid	$⊢ \neg Z \in A \to {{(x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z)}^{-1} ↾}_{A} = \emptyset$
65	53 64	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$
66	52 65	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$
67		un0	$⊢ g^{-1} \cup \emptyset = g^{-1}$
68	66 67	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}$
69	47 68	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}$
70	69	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})$
71	43 70	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})$
72		vex	$⊢ g \in V$
73		nnex	$⊢ ℕ \in V$
74		difexg	$⊢ ℕ \in V \to ℕ ∖ (1 \dots \|A\|) \in V$
75	73 74	ax-mp	$⊢ ℕ ∖ (1 \dots \|A\|) \in V$
76	75	mptex	$⊢ (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z) \in V$
77	72 76	unex	$⊢ g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z) \in V$
78		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\})$
79		rneq	$⊢ f = g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z) \to ran f = ran (g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z))$
80	79	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)))$
81		cnveq	$⊢ f = g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z) \to f^{-1} = {(g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z))}^{-1}$
82		eqidd	$⊢ f = g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z) \to A = A$
83	81 82	reseq12d	$⊢ f = g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z) \to {f^{-1} ↾}_{A} = {{(g \cup (x \in (ℕ ∖ (1 \dots \|A\|)) ⟼ Z))}^{-1} ↾}_{A}$
84	83	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}))$
85	78 80 84	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})))$
86	77 85	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}))$
87	28 40 71 86	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}))$
88	87	ex	$⊢ (A ≺ ω \land Z \in V \land \neg Z \in A) \to (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})))$
89	2 3 10 88	exlimimdd	$⊢ (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}))$
90	89	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})))$
91		nnenom	$⊢ ℕ \approx ω$
92		simpl	$⊢ (A \approx ω \land Z \in V) \to A \approx ω$
93	92	ensymd	$⊢ (A \approx ω \land Z \in V) \to ω \approx A$
94		entr	$⊢ (ℕ \approx ω \land ω \approx A) \to ℕ \approx A$
95	91 93 94	sylancr	$⊢ (A \approx ω \land Z \in V) \to ℕ \approx A$
96		bren	$⊢ ℕ \approx A \leftrightarrow \exists f f : ℕ \underset{1-1 onto}{⟶} A$
97	95 96	sylib	$⊢ (A \approx ω \land Z \in V) \to \exists f f : ℕ \underset{1-1 onto}{⟶} A$
98		nfv	$⊢ Ⅎ f (A \approx ω \land Z \in V)$
99		simpr	$⊢ ((A \approx ω \land Z \in V) \land f : ℕ \underset{1-1 onto}{⟶} A) \to f : ℕ \underset{1-1 onto}{⟶} A$
100		f1of	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to f : ℕ ⟶ A$
101		ssun1	$⊢ A \subseteq A \cup \{Z\}$
102		fss	$⊢ (f : ℕ ⟶ A \land A \subseteq A \cup \{Z\}) \to f : ℕ ⟶ A \cup \{Z\}$
103	101 102	mpan2	$⊢ f : ℕ ⟶ A \to f : ℕ ⟶ A \cup \{Z\}$
104	99 100 103	3syl	$⊢ ((A \approx ω \land Z \in V) \land f : ℕ \underset{1-1 onto}{⟶} A) \to f : ℕ ⟶ A \cup \{Z\}$
105		f1ofo	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to f : ℕ \underset{onto}{⟶} A$
106		forn	$⊢ f : ℕ \underset{onto}{⟶} A \to ran f = A$
107	99 105 106	3syl	$⊢ ((A \approx ω \land Z \in V) \land f : ℕ \underset{1-1 onto}{⟶} A) \to ran f = A$
108	29 107	sseqtrrid	$⊢ ((A \approx ω \land Z \in V) \land f : ℕ \underset{1-1 onto}{⟶} A) \to A \subseteq ran f$
109		f1ocnv	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to f^{-1} : A \underset{1-1 onto}{⟶} ℕ$
110		f1of1	$⊢ f^{-1} : A \underset{1-1 onto}{⟶} ℕ \to f^{-1} : A \underset{1-1}{⟶} ℕ$
111	99 109 110	3syl	$⊢ ((A \approx ω \land Z \in V) \land f : ℕ \underset{1-1 onto}{⟶} A) \to f^{-1} : A \underset{1-1}{⟶} ℕ$
112		f1ores	$⊢ (f^{-1} : A \underset{1-1}{⟶} ℕ \land A \subseteq A) \to ({f^{-1} ↾}_{A}) : A \underset{1-1 onto}{⟶} f^{-1} [A]$
113	29 112	mpan2	$⊢ f^{-1} : A \underset{1-1}{⟶} ℕ \to ({f^{-1} ↾}_{A}) : A \underset{1-1 onto}{⟶} f^{-1} [A]$
114		f1ofun	$⊢ ({f^{-1} ↾}_{A}) : A \underset{1-1 onto}{⟶} f^{-1} [A] \to Fun ({f^{-1} ↾}_{A})$
115	111 113 114	3syl	$⊢ ((A \approx ω \land Z \in V) \land f : ℕ \underset{1-1 onto}{⟶} A) \to Fun ({f^{-1} ↾}_{A})$
116	104 108 115	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}))$
117	116	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})))$
118	98 117	eximd	$⊢ (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})))$
119	97 118	mpd	$⊢ (A \approx ω \land Z \in V) \to \exists f (f : ℕ ⟶ A \cup \{Z\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))$
120	119	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})))$
121	90 120	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})))$
122	121	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}))$
123	1 122	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