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 35423

Description: Lemma for satffunlem1lem1 35424 and satffunlem2lem1 35426. (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 2756	. . . . . . . 8 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
2		fvex 6889	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑢) ∈ V
3		fvex 6889	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑣) ∈ V
4		gonafv 35372	. . . . . . . . . . . 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 6889	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑠) ∈ V
7		fvex 6889	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑟) ∈ V
8		gonafv 35372	. . . . . . . . . . . 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 2753	. . . . . . . . . 10 ⊢ (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
11		1oex 8490	. . . . . . . . . . 11 ⊢ 1_o ∈ V
12		opex 5439	. . . . . . . . . . 11 ⊢ ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ ∈ V
13	11, 12	opth 5451	. . . . . . . . . 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 5451	. . . . . . . . . . 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 8045	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑠 ∈ 𝑍) → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠))
18	17	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑠 ∈ 𝑍 → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
19		funfv1st2nd 8045	. . . . . . . . . . . . . . . . . . 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 8045	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑢 ∈ 𝑍) → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢))
23	22	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑢 ∈ 𝑍 → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
24		funfv1st2nd 8045	. . . . . . . . . . . . . . . . . . 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 6876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑠) = (1^st ‘𝑢) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
28	27	eqcoms 2743	. . . . . . . . . . . . . . . . . . . . . . . 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 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ↔ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠)))
31		fveq2 6876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑟) = (1^st ‘𝑣) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
32	31	eqcoms 2743	. . . . . . . . . . . . . . . . . . . . . . . 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 2737	. . . . . . . . . . . . . . . . . . . . . 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 2756	. . . . . . . . . . . . . . . . . . . . . 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 2756	. . . . . . . . . . . . . . . . . . . . . 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 4196	. . . . . . . . . . . . . . . . . . . 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 4101	. . . . . . . . . . . . 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 2752	. . . . . . . . . . . . 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 1540 ∈ wcel 2108 Vcvv 3459 ∖ cdif 3923 ∩ cin 3925 ⟨cop 4607 Fun wfun 6525 ‘cfv 6531 (class class class)co 7405 ωcom 7861 1^st c1st 7986 2^nd c2nd 7987 1_oc1o 8473 ↑_m cmap 8840 ⊼_𝑔cgna 35356

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402 ax-un 7729

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-suc 6358 df-iota 6484 df-fun 6533 df-fv 6539 df-ov 7408 df-1st 7988 df-2nd 7989 df-1o 8480 df-gona 35363

This theorem is referenced by: satffunlem1lem1 35424 satffunlem2lem1 35426

W3C validator