degenmgm2nfun

Description: The operation of a second degenerate magma is not a function. (Contributed by AV, 21-Aug-2026)

		Ref	Expression
	Hypothesis	degenmgm2.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1_o } ⟩ , ⟨ ( +_g ‘ ndx ) , { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ⟩ }
	Assertion	degenmgm2nfun	⊢ ¬ Fun ( +_g ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		degenmgm2.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1_o } ⟩ , ⟨ ( +_g ‘ ndx ) , { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ⟩ }
2		2oex	⊢ 2_o ∈ V
3		opeq2	⊢ ( 𝑧 = 2_o → ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ = ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ )
4	3	eleq1d	⊢ ( 𝑧 = 2_o → ( ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ↔ ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) )
5	4	anbi2d	⊢ ( 𝑧 = 2_o → ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ↔ ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ) )
6		eqeq2	⊢ ( 𝑧 = 2_o → ( 1_o = 𝑧 ↔ 1_o = 2_o ) )
7	6	necon3bbid	⊢ ( 𝑧 = 2_o → ( ¬ 1_o = 𝑧 ↔ 1_o ≠ 2_o ) )
8	5 7	anbi12d	⊢ ( 𝑧 = 2_o → ( ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ ¬ 1_o = 𝑧 ) ↔ ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ 1_o ≠ 2_o ) ) )
9		opex	⊢ ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ V
10	9	tpid2	⊢ ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ }
11		opex	⊢ ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ ∈ V
12	11	tpid3	⊢ ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ }
13	10 12	pm3.2i	⊢ ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } )
14		1one2o	⊢ 1_o ≠ 2_o
15	13 14	pm3.2i	⊢ ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ 1_o ≠ 2_o )
16	2 8 15	ceqsexv2d	⊢ ∃ 𝑧 ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ ¬ 1_o = 𝑧 )
17		opex	⊢ ⟨ 1_o , 2_o ⟩ ∈ V
18		1oex	⊢ 1_o ∈ V
19		opeq12	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ )
20	19	eleq1d	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ↔ ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) )
21		opeq1	⊢ ( 𝑥 = ⟨ 1_o , 2_o ⟩ → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ )
22	21	adantr	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ )
23	22	eleq1d	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ↔ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) )
24	20 23	anbi12d	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ↔ ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ) )
25		eqeq1	⊢ ( 𝑦 = 1_o → ( 𝑦 = 𝑧 ↔ 1_o = 𝑧 ) )
26	25	adantl	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( 𝑦 = 𝑧 ↔ 1_o = 𝑧 ) )
27	24 26	imbi12d	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 1_o = 𝑧 ) ) )
28	27	notbid	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ¬ ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 1_o = 𝑧 ) ) )
29		pm4.61	⊢ ( ¬ ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 1_o = 𝑧 ) ↔ ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ ¬ 1_o = 𝑧 ) )
30	28 29	bitrdi	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ ¬ 1_o = 𝑧 ) ) )
31	30	exbidv	⊢ ( ( 𝑥 = ⟨ 1_o , 2_o ⟩ ∧ 𝑦 = 1_o ) → ( ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑧 ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ ¬ 1_o = 𝑧 ) ) )
32	17 18 31	spc2ev	⊢ ( ∃ 𝑧 ( ( ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ ⟨ 1_o , 2_o ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) ∧ ¬ 1_o = 𝑧 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) )
33	16 32	ax-mp	⊢ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 )
34		exnal	⊢ ( ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) )
35	34	bicomi	⊢ ( ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) )
36	35	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) )
37	33 36	mpbir	⊢ ∃ 𝑥 ∃ 𝑦 ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 )
38		2nalexn	⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) )
39	37 38	mpbir	⊢ ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 )
40	39	intnan	⊢ ¬ ( Rel { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) )
41		tpex	⊢ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∈ V
42	1	grpplusg	⊢ ( { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∈ V → { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } = ( +_g ‘ 𝑀 ) )
43	41 42	ax-mp	⊢ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } = ( +_g ‘ 𝑀 )
44	43	eqcomi	⊢ ( +_g ‘ 𝑀 ) = { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ }
45	44	funeqi	⊢ ( Fun ( +_g ‘ 𝑀 ) ↔ Fun { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } )
46		dffun4	⊢ ( Fun { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ↔ ( Rel { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ) )
47	45 46	bitri	⊢ ( Fun ( +_g ‘ 𝑀 ) ↔ ( Rel { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 2_o ⟩ } ) → 𝑦 = 𝑧 ) ) )
48	40 47	mtbir	⊢ ¬ Fun ( +_g ‘ 𝑀 )

Metamath Proof Explorer

Theorem degenmgm2nfun

Proof