satffunlem - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > satffunlem		Structured version Visualization version GIF version

Theorem satffunlem 33048

Description: Lemma for satffunlem1lem1 33049 and satffunlem2lem1 33051. (Contributed by AV, 27-Oct-2023.)

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

**Proof of Theorem satffunlem**
Step	Hyp	Ref	Expression
1		eqtr2 2758	. . . . . . . 8 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
2		fvex 6719	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑢) ∈ V
3		fvex 6719	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑣) ∈ V
4		gonafv 32997	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑢) ∈ V ∧ (1^st ‘𝑣) ∈ V) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩)
5	2, 3, 4	mp2an 692	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩
6		fvex 6719	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑠) ∈ V
7		fvex 6719	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑟) ∈ V
8		gonafv 32997	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑠) ∈ V ∧ (1^st ‘𝑟) ∈ V) → ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
9	6, 7, 8	mp2an 692	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩
10	5, 9	eqeq12i 2752	. . . . . . . . . 10 ⊢ (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
11		1oex 8204	. . . . . . . . . . 11 ⊢ 1_o ∈ V
12		opex 5337	. . . . . . . . . . 11 ⊢ ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ ∈ V
13	11, 12	opth 5349	. . . . . . . . . 10 ⊢ (⟨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 5349	. . . . . . . . . . 11 ⊢ (⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ = ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩ ↔ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)))
15	14	anbi2i 626	. . . . . . . . . 10 ⊢ ((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 300	. . . . . . . . 9 ⊢ (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ (1_o = 1_o ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))))
17		funfv1st2nd 7806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑠 ∈ 𝑍) → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠))
18	17	ex 416	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑠 ∈ 𝑍 → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
19		funfv1st2nd 7806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑟 ∈ 𝑍) → (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟))
20	19	ex 416	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑟 ∈ 𝑍 → (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟)))
21	18, 20	anim12d 612	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟))))
22		funfv1st2nd 7806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑢 ∈ 𝑍) → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢))
23	22	ex 416	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑢 ∈ 𝑍 → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
24		funfv1st2nd 7806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑣 ∈ 𝑍) → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))
25	24	ex 416	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑣 ∈ 𝑍 → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣)))
26	23, 25	anim12d 612	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑍 → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))))
27		fveq2 6706	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑠) = (1^st ‘𝑢) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
28	27	eqcoms 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
29	28	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
30	29	eqeq1d 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ↔ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠)))
31		fveq2 6706	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑟) = (1^st ‘𝑣) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
32	31	eqcoms 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑣) = (1^st ‘𝑟) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
33	32	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
34	33	eqeq1d 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟) ↔ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)))
35	30, 34	anbi12d 634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((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 633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((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 2758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
38	37	ad2ant2r 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)) ∧ ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
39		eqtr2 2758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣)) → (2^nd ‘𝑟) = (2^nd ‘𝑣))
40	39	ad2ant2l 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)) ∧ ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))) → (2^nd ‘𝑟) = (2^nd ‘𝑣))
41	38, 40	ineq12d 4118	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑍‘(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 256	. . . . . . . . . . . . . . . . . . 19 ⊢ (((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 32	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑍‘(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 11	. . . . . . . . . . . . . . . . 17 ⊢ (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 611	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑍 → (((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
46	45	expd 419	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))))
47	46	3imp1 1349	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
48	47	difeq2d 4027	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))
49	48	adantr 484	. . . . . . . . . . . 12 ⊢ ((((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 2751	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
51	50	adantl 485	. . . . . . . . . . . 12 ⊢ ((((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 260	. . . . . . . . . . 11 ⊢ ((((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) ∧ (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))) → 𝑦 = 𝑤)
53	52	exp43 440	. . . . . . . . . 10 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤))))
54	53	adantld 494	. . . . . . . . 9 ⊢ ((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 245	. . . . . . . 8 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤))))
56	1, 55	syl5 34	. . . . . . 7 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤))))
57	56	expd 419	. . . . . 6 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤)))))
58	57	com35 98	. . . . 5 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → 𝑦 = 𝑤)))))
59	58	impd 414	. . . 4 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → 𝑦 = 𝑤))))
60	59	com24 95	. . 3 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → 𝑦 = 𝑤))))
61	60	impd 414	. 2 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → 𝑦 = 𝑤)))
62	61	3imp 1113	1 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))) → 𝑦 = 𝑤)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 Vcvv 3401 ∖ cdif 3854 ∩ cin 3856 ⟨cop 4537 Fun wfun 6363 ‘cfv 6369 (class class class)co 7202 ωcom 7633 1^st c1st 7748 2^nd c2nd 7749 1_oc1o 8184 ↑_m cmap 8497 ⊼_𝑔cgna 32981

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-sep 5181 ax-nul 5188 ax-pr 5311 ax-un 7512

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3403 df-sbc 3688 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-sn 4532 df-pr 4534 df-op 4538 df-uni 4810 df-br 5044 df-opab 5106 df-mpt 5125 df-id 5444 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-suc 6208 df-iota 6327 df-fun 6371 df-fv 6377 df-ov 7205 df-1st 7750 df-2nd 7751 df-1o 8191 df-gona 32988

This theorem is referenced by: satffunlem1lem1 33049 satffunlem2lem1 33051

W3C validator