satffunlem

		Ref	Expression
	Assertion	satffunlem	⊢ ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) → 𝑦 = 𝑤 )

Proof

Step	Hyp	Ref	Expression
1		eqtr2	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) )
2		fvex	⊢ ( 1^st ‘ 𝑢 ) ∈ V
3		fvex	⊢ ( 1^st ‘ 𝑣 ) ∈ V
4		gonafv	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ V ∧ ( 1^st ‘ 𝑣 ) ∈ V ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
5	2 3 4	mp2an	⊢ ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩
6		fvex	⊢ ( 1^st ‘ 𝑠 ) ∈ V
7		fvex	⊢ ( 1^st ‘ 𝑟 ) ∈ V
8		gonafv	⊢ ( ( ( 1^st ‘ 𝑠 ) ∈ V ∧ ( 1^st ‘ 𝑟 ) ∈ V ) → ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ )
9	6 7 8	mp2an	⊢ ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩
10	5 9	eqeq12i	⊢ ( ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ↔ ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ )
11		1oex	⊢ 1_o ∈ V
12		opex	⊢ ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ∈ V
13	11 12	opth	⊢ ( ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ ↔ ( 1_o = 1_o ∧ ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ = ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ) )
14	2 3	opth	⊢ ( ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ = ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ↔ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) )
15	14	anbi2i	⊢ ( ( 1_o = 1_o ∧ ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ = ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ) ↔ ( 1_o = 1_o ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) )
16	10 13 15	3bitri	⊢ ( ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ↔ ( 1_o = 1_o ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) )
17		funfv1st2nd	⊢ ( ( Fun 𝑍 ∧ 𝑠 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) )
18	17	ex	⊢ ( Fun 𝑍 → ( 𝑠 ∈ 𝑍 → ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) )
19		funfv1st2nd	⊢ ( ( Fun 𝑍 ∧ 𝑟 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) )
20	19	ex	⊢ ( Fun 𝑍 → ( 𝑟 ∈ 𝑍 → ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ) )
21	18 20	anim12d	⊢ ( Fun 𝑍 → ( ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) → ( ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ) ) )
22		funfv1st2nd	⊢ ( ( Fun 𝑍 ∧ 𝑢 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) )
23	22	ex	⊢ ( Fun 𝑍 → ( 𝑢 ∈ 𝑍 → ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ) )
24		funfv1st2nd	⊢ ( ( Fun 𝑍 ∧ 𝑣 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) )
25	24	ex	⊢ ( Fun 𝑍 → ( 𝑣 ∈ 𝑍 → ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) )
26	23 25	anim12d	⊢ ( Fun 𝑍 → ( ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) → ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) )
27		fveq2	⊢ ( ( 1^st ‘ 𝑠 ) = ( 1^st ‘ 𝑢 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) )
28	27	eqcoms	⊢ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) )
29	28	adantr	⊢ ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) )
30	29	eqeq1d	⊢ ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ↔ ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑠 ) ) )
31		fveq2	⊢ ( ( 1^st ‘ 𝑟 ) = ( 1^st ‘ 𝑣 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) )
32	31	eqcoms	⊢ ( ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) → ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) )
33	32	adantl	⊢ ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) )
34	33	eqeq1d	⊢ ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ↔ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑟 ) ) )
35	30 34	anbi12d	⊢ ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ) ↔ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑟 ) ) ) )
36	35	anbi1d	⊢ ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) ↔ ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) ) )
37		eqtr2	⊢ ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ) → ( 2^nd ‘ 𝑠 ) = ( 2^nd ‘ 𝑢 ) )
38	37	ad2ant2r	⊢ ( ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) → ( 2^nd ‘ 𝑠 ) = ( 2^nd ‘ 𝑢 ) )
39		eqtr2	⊢ ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑟 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) → ( 2^nd ‘ 𝑟 ) = ( 2^nd ‘ 𝑣 ) )
40	39	ad2ant2l	⊢ ( ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) → ( 2^nd ‘ 𝑟 ) = ( 2^nd ‘ 𝑣 ) )
41	38 40	ineq12d	⊢ ( ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) → ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) = ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
42	36 41	syl6bi	⊢ ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) → ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) = ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
43	42	com12	⊢ ( ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) → ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) = ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
44	43	a1i	⊢ ( Fun 𝑍 → ( ( ( ( 𝑍 ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑟 ) ) = ( 2^nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1^st ‘ 𝑣 ) ) = ( 2^nd ‘ 𝑣 ) ) ) → ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) = ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
45	21 26 44	syl2and	⊢ ( Fun 𝑍 → ( ( ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) = ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
46	45	expd	⊢ ( Fun 𝑍 → ( ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) → ( ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) → ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) = ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) )
47	46	3imp1	⊢ ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) → ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) = ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
48	47	difeq2d	⊢ ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) → ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
49	48	adantr	⊢ ( ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) ∧ ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) → ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
50		eqeq12	⊢ ( ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( 𝑦 = 𝑤 ↔ ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
51	50	adantl	⊢ ( ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) ∧ ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) → ( 𝑦 = 𝑤 ↔ ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
52	49 51	mpbird	⊢ ( ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) ∧ ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) → 𝑦 = 𝑤 )
53	52	exp43	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) )
54	53	adantld	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 1_o = 1_o ∧ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ∧ ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) )
55	16 54	syl5bi	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) )
56	1 55	syl5	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) )
57	56	expd	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) ) )
58	57	com35	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → 𝑦 = 𝑤 ) ) ) ) )
59	58	impd	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → 𝑦 = 𝑤 ) ) ) )
60	59	com24	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → 𝑦 = 𝑤 ) ) ) )
61	60	impd	⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → 𝑦 = 𝑤 ) ) )
62	61	3imp	⊢ ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) → 𝑦 = 𝑤 )

Metamath Proof Explorer

Theorem satffunlem

Proof