dif1enlem

Description: Lemma for rexdif1en and dif1en . (Contributed by BTernaryTau, 18-Aug-2024) Generalize to all ordinals and add a sethood requirement to avoid ax-un . (Revised by BTernaryTau, 5-Jan-2025)

		Ref	Expression
	Assertion	dif1enlem	$⊢ ((F \in V \land A \in W \land M \in On) \land F : A \underset{1-1 onto}{⟶} suc M) \to (A ∖ \{F^{-1} (M)\}) \approx M$

Proof

Step	Hyp	Ref	Expression
1		sucidg	$⊢ M \in On \to M \in suc M$
2		dff1o3	$⊢ F : A \underset{1-1 onto}{⟶} suc M \leftrightarrow (F : A \underset{onto}{⟶} suc M \land Fun F^{-1})$
3	2	simprbi	$⊢ F : A \underset{1-1 onto}{⟶} suc M \to Fun F^{-1}$
4	3	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to Fun F^{-1}$
5		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} suc M \to F : A \underset{onto}{⟶} suc M$
6		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} suc M \to F Fn A$
7		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
8		foeq1	$⊢ {F ↾}_{A} = F \to (({F ↾}_{A}) : A \underset{onto}{⟶} suc M \leftrightarrow F : A \underset{onto}{⟶} suc M)$
9	6 7 8	3syl	$⊢ F : A \underset{1-1 onto}{⟶} suc M \to (({F ↾}_{A}) : A \underset{onto}{⟶} suc M \leftrightarrow F : A \underset{onto}{⟶} suc M)$
10	5 9	mpbird	$⊢ F : A \underset{1-1 onto}{⟶} suc M \to ({F ↾}_{A}) : A \underset{onto}{⟶} suc M$
11	10	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ({F ↾}_{A}) : A \underset{onto}{⟶} suc M$
12	6	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to F Fn A$
13		f1ocnvdm	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to F^{-1} (M) \in A$
14		f1ocnvfv2	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to F (F^{-1} (M)) = M$
15		snidg	$⊢ M \in suc M \to M \in \{M\}$
16	15	adantl	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to M \in \{M\}$
17	14 16	eqeltrd	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to F (F^{-1} (M)) \in \{M\}$
18		fressnfv	$⊢ (F Fn A \land F^{-1} (M) \in A) \to (({F ↾}_{\{F^{-1} (M)\}}) : \{F^{-1} (M)\} ⟶ \{M\} \leftrightarrow F (F^{-1} (M)) \in \{M\})$
19	18	biimp3ar	$⊢ (F Fn A \land F^{-1} (M) \in A \land F (F^{-1} (M)) \in \{M\}) \to ({F ↾}_{\{F^{-1} (M)\}}) : \{F^{-1} (M)\} ⟶ \{M\}$
20	12 13 17 19	syl3anc	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ({F ↾}_{\{F^{-1} (M)\}}) : \{F^{-1} (M)\} ⟶ \{M\}$
21		disjsn	$⊢ A \cap \{F^{-1} (M)\} = \emptyset \leftrightarrow \neg F^{-1} (M) \in A$
22	21	con2bii	$⊢ F^{-1} (M) \in A \leftrightarrow \neg A \cap \{F^{-1} (M)\} = \emptyset$
23	13 22	sylib	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to \neg A \cap \{F^{-1} (M)\} = \emptyset$
24		fnresdisj	$⊢ F Fn A \to (A \cap \{F^{-1} (M)\} = \emptyset \leftrightarrow {F ↾}_{\{F^{-1} (M)\}} = \emptyset)$
25	6 24	syl	$⊢ F : A \underset{1-1 onto}{⟶} suc M \to (A \cap \{F^{-1} (M)\} = \emptyset \leftrightarrow {F ↾}_{\{F^{-1} (M)\}} = \emptyset)$
26	25	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to (A \cap \{F^{-1} (M)\} = \emptyset \leftrightarrow {F ↾}_{\{F^{-1} (M)\}} = \emptyset)$
27	23 26	mtbid	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to \neg {F ↾}_{\{F^{-1} (M)\}} = \emptyset$
28	27	neqned	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to {F ↾}_{\{F^{-1} (M)\}} \neq \emptyset$
29		foconst	$⊢ (({F ↾}_{\{F^{-1} (M)\}}) : \{F^{-1} (M)\} ⟶ \{M\} \land {F ↾}_{\{F^{-1} (M)\}} \neq \emptyset) \to ({F ↾}_{\{F^{-1} (M)\}}) : \{F^{-1} (M)\} \underset{onto}{⟶} \{M\}$
30	20 28 29	syl2anc	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ({F ↾}_{\{F^{-1} (M)\}}) : \{F^{-1} (M)\} \underset{onto}{⟶} \{M\}$
31		resdif	$⊢ (Fun F^{-1} \land ({F ↾}_{A}) : A \underset{onto}{⟶} suc M \land ({F ↾}_{\{F^{-1} (M)\}}) : \{F^{-1} (M)\} \underset{onto}{⟶} \{M\}) \to ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} suc M ∖ \{M\}$
32	4 11 30 31	syl3anc	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} suc M ∖ \{M\}$
33	1 32	sylan2	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in On) \to ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} suc M ∖ \{M\}$
34		eloni	$⊢ M \in On \to Ord M$
35		orddif	$⊢ Ord M \to M = suc M ∖ \{M\}$
36	34 35	syl	$⊢ M \in On \to M = suc M ∖ \{M\}$
37	36	f1oeq3d	$⊢ M \in On \to (({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M \leftrightarrow ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} suc M ∖ \{M\})$
38	37	adantl	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in On) \to (({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M \leftrightarrow ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} suc M ∖ \{M\})$
39	33 38	mpbird	$⊢ (F : A \underset{1-1 onto}{⟶} suc M \land M \in On) \to ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M$
40	39	ancoms	$⊢ (M \in On \land F : A \underset{1-1 onto}{⟶} suc M) \to ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M$
41	40	3ad2antl3	$⊢ ((F \in V \land A \in W \land M \in On) \land F : A \underset{1-1 onto}{⟶} suc M) \to ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M$
42		difexg	$⊢ A \in W \to A ∖ \{F^{-1} (M)\} \in V$
43		resexg	$⊢ F \in V \to {F ↾}_{(A ∖ \{F^{-1} (M)\})} \in V$
44		f1oen4g	$⊢ (({F ↾}_{(A ∖ \{F^{-1} (M)\})} \in V \land A ∖ \{F^{-1} (M)\} \in V \land M \in On) \land ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M) \to (A ∖ \{F^{-1} (M)\}) \approx M$
45	43 44	syl3anl1	$⊢ ((F \in V \land A ∖ \{F^{-1} (M)\} \in V \land M \in On) \land ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M) \to (A ∖ \{F^{-1} (M)\}) \approx M$
46	42 45	syl3anl2	$⊢ ((F \in V \land A \in W \land M \in On) \land ({F ↾}_{(A ∖ \{F^{-1} (M)\})}) : A ∖ \{F^{-1} (M)\} \underset{1-1 onto}{⟶} M) \to (A ∖ \{F^{-1} (M)\}) \approx M$
47	41 46	syldan	$⊢ ((F \in V \land A \in W \land M \in On) \land F : A \underset{1-1 onto}{⟶} suc M) \to (A ∖ \{F^{-1} (M)\}) \approx M$

Metamath Proof Explorer

Theorem dif1enlem

Proof