noextenddif

Description: Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021)

		Ref	Expression
	Hypothesis	noextend.1	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\}$
	Assertion	noextenddif	$⊢ A \in No \to ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} = dom A$

Proof

Step	Hyp	Ref	Expression
1		noextend.1	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\}$
2		nodmon	$⊢ A \in No \to dom A \in On$
3	1	nosgnn0i	$⊢ \emptyset \neq X$
4	3	a1i	$⊢ A \in No \to \emptyset \neq X$
5		nodmord	$⊢ A \in No \to Ord dom A$
6		ordirr	$⊢ Ord dom A \to \neg dom A \in dom A$
7	5 6	syl	$⊢ A \in No \to \neg dom A \in dom A$
8		ndmfv	$⊢ \neg dom A \in dom A \to A (dom A) = \emptyset$
9	7 8	syl	$⊢ A \in No \to A (dom A) = \emptyset$
10		nofun	$⊢ A \in No \to Fun A$
11		funfn	$⊢ Fun A \leftrightarrow A Fn dom A$
12	10 11	sylib	$⊢ A \in No \to A Fn dom A$
13		fnsng	$⊢ (dom A \in On \land X \in \{1_{𝑜}, 2_{𝑜}\}) \to \{⟨dom A, X⟩\} Fn \{dom A\}$
14	2 1 13	sylancl	$⊢ A \in No \to \{⟨dom A, X⟩\} Fn \{dom A\}$
15		disjsn	$⊢ dom A \cap \{dom A\} = \emptyset \leftrightarrow \neg dom A \in dom A$
16	7 15	sylibr	$⊢ A \in No \to dom A \cap \{dom A\} = \emptyset$
17		snidg	$⊢ dom A \in On \to dom A \in \{dom A\}$
18	2 17	syl	$⊢ A \in No \to dom A \in \{dom A\}$
19		fvun2	$⊢ (A Fn dom A \land \{⟨dom A, X⟩\} Fn \{dom A\} \land (dom A \cap \{dom A\} = \emptyset \land dom A \in \{dom A\})) \to (A \cup \{⟨dom A, X⟩\}) (dom A) = \{⟨dom A, X⟩\} (dom A)$
20	12 14 16 18 19	syl112anc	$⊢ A \in No \to (A \cup \{⟨dom A, X⟩\}) (dom A) = \{⟨dom A, X⟩\} (dom A)$
21		fvsng	$⊢ (dom A \in On \land X \in \{1_{𝑜}, 2_{𝑜}\}) \to \{⟨dom A, X⟩\} (dom A) = X$
22	2 1 21	sylancl	$⊢ A \in No \to \{⟨dom A, X⟩\} (dom A) = X$
23	20 22	eqtrd	$⊢ A \in No \to (A \cup \{⟨dom A, X⟩\}) (dom A) = X$
24	4 9 23	3netr4d	$⊢ A \in No \to A (dom A) \neq (A \cup \{⟨dom A, X⟩\}) (dom A)$
25		fveq2	$⊢ x = dom A \to A (x) = A (dom A)$
26		fveq2	$⊢ x = dom A \to (A \cup \{⟨dom A, X⟩\}) (x) = (A \cup \{⟨dom A, X⟩\}) (dom A)$
27	25 26	neeq12d	$⊢ x = dom A \to (A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x) \leftrightarrow A (dom A) \neq (A \cup \{⟨dom A, X⟩\}) (dom A))$
28	27	onintss	$⊢ dom A \in On \to (A (dom A) \neq (A \cup \{⟨dom A, X⟩\}) (dom A) \to ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} \subseteq dom A)$
29	2 24 28	sylc	$⊢ A \in No \to ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} \subseteq dom A$
30		eloni	$⊢ y \in On \to Ord y$
31		ordtri2	$⊢ (Ord y \land Ord dom A) \to (y \in dom A \leftrightarrow \neg (y = dom A \lor dom A \in y))$
32		eqcom	$⊢ y = dom A \leftrightarrow dom A = y$
33	32	orbi1i	$⊢ (y = dom A \lor dom A \in y) \leftrightarrow (dom A = y \lor dom A \in y)$
34		orcom	$⊢ (dom A = y \lor dom A \in y) \leftrightarrow (dom A \in y \lor dom A = y)$
35	33 34	bitri	$⊢ (y = dom A \lor dom A \in y) \leftrightarrow (dom A \in y \lor dom A = y)$
36	35	notbii	$⊢ \neg (y = dom A \lor dom A \in y) \leftrightarrow \neg (dom A \in y \lor dom A = y)$
37	31 36	bitrdi	$⊢ (Ord y \land Ord dom A) \to (y \in dom A \leftrightarrow \neg (dom A \in y \lor dom A = y))$
38		ordsseleq	$⊢ (Ord dom A \land Ord y) \to (dom A \subseteq y \leftrightarrow (dom A \in y \lor dom A = y))$
39	38	notbid	$⊢ (Ord dom A \land Ord y) \to (\neg dom A \subseteq y \leftrightarrow \neg (dom A \in y \lor dom A = y))$
40	39	ancoms	$⊢ (Ord y \land Ord dom A) \to (\neg dom A \subseteq y \leftrightarrow \neg (dom A \in y \lor dom A = y))$
41	37 40	bitr4d	$⊢ (Ord y \land Ord dom A) \to (y \in dom A \leftrightarrow \neg dom A \subseteq y)$
42	30 5 41	syl2anr	$⊢ (A \in No \land y \in On) \to (y \in dom A \leftrightarrow \neg dom A \subseteq y)$
43	12	3ad2ant1	$⊢ (A \in No \land y \in On \land y \in dom A) \to A Fn dom A$
44	14	3ad2ant1	$⊢ (A \in No \land y \in On \land y \in dom A) \to \{⟨dom A, X⟩\} Fn \{dom A\}$
45	16	3ad2ant1	$⊢ (A \in No \land y \in On \land y \in dom A) \to dom A \cap \{dom A\} = \emptyset$
46		simp3	$⊢ (A \in No \land y \in On \land y \in dom A) \to y \in dom A$
47		fvun1	$⊢ (A Fn dom A \land \{⟨dom A, X⟩\} Fn \{dom A\} \land (dom A \cap \{dom A\} = \emptyset \land y \in dom A)) \to (A \cup \{⟨dom A, X⟩\}) (y) = A (y)$
48	43 44 45 46 47	syl112anc	$⊢ (A \in No \land y \in On \land y \in dom A) \to (A \cup \{⟨dom A, X⟩\}) (y) = A (y)$
49	48	eqcomd	$⊢ (A \in No \land y \in On \land y \in dom A) \to A (y) = (A \cup \{⟨dom A, X⟩\}) (y)$
50	49	3expia	$⊢ (A \in No \land y \in On) \to (y \in dom A \to A (y) = (A \cup \{⟨dom A, X⟩\}) (y))$
51	42 50	sylbird	$⊢ (A \in No \land y \in On) \to (\neg dom A \subseteq y \to A (y) = (A \cup \{⟨dom A, X⟩\}) (y))$
52	51	necon1ad	$⊢ (A \in No \land y \in On) \to (A (y) \neq (A \cup \{⟨dom A, X⟩\}) (y) \to dom A \subseteq y)$
53	52	ralrimiva	$⊢ A \in No \to \forall y \in On (A (y) \neq (A \cup \{⟨dom A, X⟩\}) (y) \to dom A \subseteq y)$
54		fveq2	$⊢ x = y \to A (x) = A (y)$
55		fveq2	$⊢ x = y \to (A \cup \{⟨dom A, X⟩\}) (x) = (A \cup \{⟨dom A, X⟩\}) (y)$
56	54 55	neeq12d	$⊢ x = y \to (A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x) \leftrightarrow A (y) \neq (A \cup \{⟨dom A, X⟩\}) (y))$
57	56	ralrab	$⊢ \forall y \in \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} dom A \subseteq y \leftrightarrow \forall y \in On (A (y) \neq (A \cup \{⟨dom A, X⟩\}) (y) \to dom A \subseteq y)$
58	53 57	sylibr	$⊢ A \in No \to \forall y \in \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} dom A \subseteq y$
59		ssint	$⊢ dom A \subseteq ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} \leftrightarrow \forall y \in \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} dom A \subseteq y$
60	58 59	sylibr	$⊢ A \in No \to dom A \subseteq ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\}$
61	29 60	eqssd	$⊢ A \in No \to ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, X⟩\}) (x)\} = dom A$

Metamath Proof Explorer

Theorem noextenddif

Proof