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 33995

Description: Lemma for satffunlem1lem1 33996 and satffunlem2lem1 33998. (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 2760	. . . . . . . 8 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
2		fvex 6855	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑢) ∈ V
3		fvex 6855	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑣) ∈ V
4		gonafv 33944	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑢) ∈ V ∧ (1^st ‘𝑣) ∈ V) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩)
5	2, 3, 4	mp2an 690	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩
6		fvex 6855	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑠) ∈ V
7		fvex 6855	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑟) ∈ V
8		gonafv 33944	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑠) ∈ V ∧ (1^st ‘𝑟) ∈ V) → ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
9	6, 7, 8	mp2an 690	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩
10	5, 9	eqeq12i 2754	. . . . . . . . . 10 ⊢ (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
11		1oex 8422	. . . . . . . . . . 11 ⊢ 1_o ∈ V
12		opex 5421	. . . . . . . . . . 11 ⊢ ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ ∈ V
13	11, 12	opth 5433	. . . . . . . . . 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 5433	. . . . . . . . . . 11 ⊢ (⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ = ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩ ↔ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)))
15	14	anbi2i 623	. . . . . . . . . 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 296	. . . . . . . . 9 ⊢ (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ (1_o = 1_o ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))))
17		funfv1st2nd 7978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑠 ∈ 𝑍) → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠))
18	17	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑠 ∈ 𝑍 → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
19		funfv1st2nd 7978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑟 ∈ 𝑍) → (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟))
20	19	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑟 ∈ 𝑍 → (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟)))
21	18, 20	anim12d 609	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟))))
22		funfv1st2nd 7978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑢 ∈ 𝑍) → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢))
23	22	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑢 ∈ 𝑍 → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
24		funfv1st2nd 7978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑣 ∈ 𝑍) → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))
25	24	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑣 ∈ 𝑍 → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣)))
26	23, 25	anim12d 609	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑍 → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))))
27		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑠) = (1^st ‘𝑢) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
28	27	eqcoms 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
29	28	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
30	29	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ↔ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠)))
31		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑟) = (1^st ‘𝑣) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
32	31	eqcoms 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑣) = (1^st ‘𝑟) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
33	32	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
34	33	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟) ↔ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)))
35	30, 34	anbi12d 631	. . . . . . . . . . . . . . . . . . . . 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 630	. . . . . . . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
38	37	ad2ant2r 745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)) ∧ ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
39		eqtr2 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣)) → (2^nd ‘𝑟) = (2^nd ‘𝑣))
40	39	ad2ant2l 744	. . . . . . . . . . . . . . . . . . . . 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 4173	. . . . . . . . . . . . . . . . . . . 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 252	. . . . . . . . . . . . . . . . . . 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 608	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑍 → (((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
46	45	expd 416	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))))
47	46	3imp1 1347	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
48	47	difeq2d 4082	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))
49	48	adantr 481	. . . . . . . . . . . 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 2753	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
51	50	adantl 482	. . . . . . . . . . . 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 256	. . . . . . . . . . 11 ⊢ ((((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) ∧ (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))) → 𝑦 = 𝑤)
53	52	exp43 437	. . . . . . . . . 10 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤))))
54	53	adantld 491	. . . . . . . . 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	biimtrid 241	. . . . . . . 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 416	. . . . . 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 411	. . . 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 411	. 2 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → 𝑦 = 𝑤)))
62	61	3imp 1111	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 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 Vcvv 3445 ∖ cdif 3907 ∩ cin 3909 ⟨cop 4592 Fun wfun 6490 ‘cfv 6496 (class class class)co 7357 ωcom 7802 1^st c1st 7919 2^nd c2nd 7920 1_oc1o 8405 ↑_m cmap 8765 ⊼_𝑔cgna 33928

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-suc 6323 df-iota 6448 df-fun 6498 df-fv 6504 df-ov 7360 df-1st 7921 df-2nd 7922 df-1o 8412 df-gona 33935

This theorem is referenced by: satffunlem1lem1 33996 satffunlem2lem1 33998

W3C validator