dif1enlem

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

Proof

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

Metamath Proof Explorer

Theorem dif1enlem

Proof