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 35914

Description: Lemma for satffunlem1lem1 35915 and satffunlem2lem1 35917. (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 2787	. . . . . . . 8 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
2		fvex 6901	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑢) ∈ V
3		fvex 6901	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑣) ∈ V
4		gonafv 35863	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑢) ∈ V ∧ (1^st ‘𝑣) ∈ V) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩)
5	2, 3, 4	mp2an 705	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩
6		fvex 6901	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑠) ∈ V
7		fvex 6901	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑟) ∈ V
8		gonafv 35863	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑠) ∈ V ∧ (1^st ‘𝑟) ∈ V) → ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
9	6, 7, 8	mp2an 705	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩
10	5, 9	eqeq12i 2784	. . . . . . . . . 10 ⊢ (((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
11		1oex 8472	. . . . . . . . . . 11 ⊢ 1_o ∈ V
12		opex 5450	. . . . . . . . . . 11 ⊢ ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ ∈ V
13	11, 12	opth 5463	. . . . . . . . . 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 5463	. . . . . . . . . . 11 ⊢ (⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩ = ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩ ↔ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)))
15	14	anbi2i 635	. . . . . . . . . 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 8052	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑠 ∈ 𝑍) → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠))
18	17	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑠 ∈ 𝑍 → (𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
19		funfv1st2nd 8052	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑟 ∈ 𝑍) → (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟))
20	19	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑟 ∈ 𝑍 → (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟)))
21	18, 20	anim12d 621	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟))))
22		funfv1st2nd 8052	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑢 ∈ 𝑍) → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢))
23	22	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑢 ∈ 𝑍 → (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
24		funfv1st2nd 8052	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑍 ∧ 𝑣 ∈ 𝑍) → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))
25	24	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝑍 → (𝑣 ∈ 𝑍 → (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣)))
26	23, 25	anim12d 621	. . . . . . . . . . . . . . . . 17 ⊢ (Fun 𝑍 → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))))
27		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑠) = (1^st ‘𝑢) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
28	27	eqcoms 2774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
29	28	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑠)) = (𝑍‘(1^st ‘𝑢)))
30	29	eqeq1d 2768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑠)) = (2^nd ‘𝑠) ↔ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠)))
31		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑟) = (1^st ‘𝑣) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
32	31	eqcoms 2774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑣) = (1^st ‘𝑟) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
33	32	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑍‘(1^st ‘𝑟)) = (𝑍‘(1^st ‘𝑣)))
34	33	eqeq1d 2768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((𝑍‘(1^st ‘𝑟)) = (2^nd ‘𝑟) ↔ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)))
35	30, 34	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 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 643	. . . . . . . . . . . . . . . . . . . 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 2787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢)) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
38	37	ad2ant2r 760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑠) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟)) ∧ ((𝑍‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣))) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
39		eqtr2 2787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑟) ∧ (𝑍‘(1^st ‘𝑣)) = (2^nd ‘𝑣)) → (2^nd ‘𝑟) = (2^nd ‘𝑣))
40	39	ad2ant2l 759	. . . . . . . . . . . . . . . . . . . . 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 4177	. . . . . . . . . . . . . . . . . . . 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 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 33	. . . . . . . . . . . . . . . . . 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 620	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑍 → (((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
46	45	expd 421	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))))
47	46	3imp1 1366	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)) = ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
48	47	difeq2d 4084	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟))) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))
49	48	adantr 486	. . . . . . . . . . . 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 2783	. . . . . . . . . . . . 13 ⊢ ((𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
51	50	adantl 487	. . . . . . . . . . . 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 442	. . . . . . . . . 10 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^st ‘𝑢) = (1^st ‘𝑠) ∧ (1^st ‘𝑣) = (1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤))))
54	53	adantld 496	. . . . . . . . 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 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 35	. . . . . . 7 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤))))
57	56	expd 421	. . . . . 6 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 = 𝑤)))))
58	57	com35 99	. . . . 5 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → (𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → 𝑦 = 𝑤)))))
59	58	impd 416	. . . 4 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → 𝑦 = 𝑤))))
60	59	com24 96	. . 3 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → 𝑦 = 𝑤))))
61	60	impd 416	. 2 ⊢ ((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → 𝑦 = 𝑤)))
62	61	3imp 1128	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

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 Vcvv 3458 ∖ cdif 3905 ∩ cin 3907 ⟨cop 4600 Fun wfun 6537 ‘cfv 6543 (class class class)co 7423 ωcom 7871 1^st c1st 7993 2^nd c2nd 7994 1_oc1o 8455 ↑_m cmap 8833 ⊼_𝑔cgna 35847

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pr 5409 ax-un 7745

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-suc 6373 df-iota 6499 df-fun 6545 df-fv 6551 df-ov 7426 df-1st 7995 df-2nd 7996 df-1o 8462 df-gona 35854

This theorem is used by: satffunlem1lem1 35915 satffunlem2lem1 35917

W3C validator