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 35443

Description: Lemma for satffunlem1lem1 35444 and satffunlem2lem1 35446. (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 2752	. . . . . . . 8 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
2		fvex 6835	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑢) ∈ V
3		fvex 6835	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑣) ∈ V
4		gonafv 35392	. . . . . . . . . . . 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 6835	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑠) ∈ V
7		fvex 6835	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑟) ∈ V
8		gonafv 35392	. . . . . . . . . . . 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 2749	. . . . . . . . . 10 ⊢ (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
11		1oex 8395	. . . . . . . . . . 11 ⊢ 1_o ∈ V
12		opex 5404	. . . . . . . . . . 11 ⊢ ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ ∈ V
13	11, 12	opth 5416	. . . . . . . . . 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 5416	. . . . . . . . . . 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 297	. . . . . . . . 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 412	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑠 ∈ 𝑍 → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
19		funfv1st2nd 7978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑟 ∈ 𝑍) → (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟))
20	19	ex 412	. . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑢 ∈ 𝑍 → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
24		funfv1st2nd 7978	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑣 ∈ 𝑍) → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))
25	24	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑣 ∈ 𝑍 → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣)))
26	23, 25	anim12d 609	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑍 → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))))
27		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑠) = (1^st ‘𝑢) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
28	27	eqcoms 2739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
29	28	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
30	29	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ↔ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠)))
31		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑟) = (1^st ‘𝑣) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
32	31	eqcoms 2739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑣) = (1^st ‘𝑟) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
33	32	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
34	33	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟) ↔ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)))
35	30, 34	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 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 631	. . . . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . . . . . . . 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 4171	. . . . . . . . . . . . . . . . . . . 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	biimtrdi 253	. . . . . . . . . . . . . . . . . . 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 415	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))))
47	46	3imp1 1348	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
48	47	difeq2d 4076	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))
49	48	adantr 480	. . . . . . . . . . . 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 2748	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
51	50	adantl 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 ‘𝑣)))))
52	49, 51	mpbird 257	. . . . . . . . . . 11 ⊢ ((((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) ∧ (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))) → 𝑦 = 𝑤)
53	52	exp43 436	. . . . . . . . . 10 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤))))
54	53	adantld 490	. . . . . . . . 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 242	. . . . . . . 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 415	. . . . . 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 410	. . . 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 410	. 2 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → 𝑦 = 𝑤)))
62	61	3imp 1110	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 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 Vcvv 3436 ∖ cdif 3899 ∩ cin 3901 ⟨cop 4582 Fun wfun 6475 ‘cfv 6481 (class class class)co 7346 ωcom 7796 1^st c1st 7919 2^nd c2nd 7920 1_oc1o 8378 ↑_m cmap 8750 ⊼_𝑔cgna 35376

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5234 ax-nul 5244 ax-pr 5370 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4476 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-br 5092 df-opab 5154 df-mpt 5173 df-id 5511 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-suc 6312 df-iota 6437 df-fun 6483 df-fv 6489 df-ov 7349 df-1st 7921 df-2nd 7922 df-1o 8385 df-gona 35383

This theorem is referenced by: satffunlem1lem1 35444 satffunlem2lem1 35446

W3C validator