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

Theorem satffunlem 34380
Description: Lemma for satffunlem1lem1 34381 and satffunlem2lem1 34383. (Contributed by AV, 27-Oct-2023.)
Assertion
Ref Expression
satffunlem (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → 𝑦 = 𝑤)

Proof of Theorem satffunlem
StepHypRef Expression
1 eqtr2 2756 . . . . . . . 8 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)))
2 fvex 6901 . . . . . . . . . . . 12 (1st𝑢) ∈ V
3 fvex 6901 . . . . . . . . . . . 12 (1st𝑣) ∈ V
4 gonafv 34329 . . . . . . . . . . . 12 (((1st𝑢) ∈ V ∧ (1st𝑣) ∈ V) → ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
52, 3, 4mp2an 690 . . . . . . . . . . 11 ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩
6 fvex 6901 . . . . . . . . . . . 12 (1st𝑠) ∈ V
7 fvex 6901 . . . . . . . . . . . 12 (1st𝑟) ∈ V
8 gonafv 34329 . . . . . . . . . . . 12 (((1st𝑠) ∈ V ∧ (1st𝑟) ∈ V) → ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
96, 7, 8mp2an 690 . . . . . . . . . . 11 ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩
105, 9eqeq12i 2750 . . . . . . . . . 10 (((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)) ↔ ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
11 1oex 8472 . . . . . . . . . . 11 1o ∈ V
12 opex 5463 . . . . . . . . . . 11 ⟨(1st𝑢), (1st𝑣)⟩ ∈ V
1311, 12opth 5475 . . . . . . . . . 10 (⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ ↔ (1o = 1o ∧ ⟨(1st𝑢), (1st𝑣)⟩ = ⟨(1st𝑠), (1st𝑟)⟩))
142, 3opth 5475 . . . . . . . . . . 11 (⟨(1st𝑢), (1st𝑣)⟩ = ⟨(1st𝑠), (1st𝑟)⟩ ↔ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)))
1514anbi2i 623 . . . . . . . . . 10 ((1o = 1o ∧ ⟨(1st𝑢), (1st𝑣)⟩ = ⟨(1st𝑠), (1st𝑟)⟩) ↔ (1o = 1o ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))))
1610, 13, 153bitri 296 . . . . . . . . 9 (((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)) ↔ (1o = 1o ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))))
17 funfv1st2nd 8028 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑠𝑍) → (𝑍‘(1st𝑠)) = (2nd𝑠))
1817ex 413 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑠𝑍 → (𝑍‘(1st𝑠)) = (2nd𝑠)))
19 funfv1st2nd 8028 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑟𝑍) → (𝑍‘(1st𝑟)) = (2nd𝑟))
2019ex 413 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑟𝑍 → (𝑍‘(1st𝑟)) = (2nd𝑟)))
2118, 20anim12d 609 . . . . . . . . . . . . . . . . 17 (Fun 𝑍 → ((𝑠𝑍𝑟𝑍) → ((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟))))
22 funfv1st2nd 8028 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑢𝑍) → (𝑍‘(1st𝑢)) = (2nd𝑢))
2322ex 413 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑢𝑍 → (𝑍‘(1st𝑢)) = (2nd𝑢)))
24 funfv1st2nd 8028 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑣𝑍) → (𝑍‘(1st𝑣)) = (2nd𝑣))
2524ex 413 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑣𝑍 → (𝑍‘(1st𝑣)) = (2nd𝑣)))
2623, 25anim12d 609 . . . . . . . . . . . . . . . . 17 (Fun 𝑍 → ((𝑢𝑍𝑣𝑍) → ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))))
27 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) = (1st𝑢) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
2827eqcoms 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑢) = (1st𝑠) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
2928adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
3029eqeq1d 2734 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((𝑍‘(1st𝑠)) = (2nd𝑠) ↔ (𝑍‘(1st𝑢)) = (2nd𝑠)))
31 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑟) = (1st𝑣) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3231eqcoms 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑣) = (1st𝑟) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3332adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3433eqeq1d 2734 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((𝑍‘(1st𝑟)) = (2nd𝑟) ↔ (𝑍‘(1st𝑣)) = (2nd𝑟)))
3530, 34anbi12d 631 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ↔ ((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟))))
3635anbi1d 630 . . . . . . . . . . . . . . . . . . . 20 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) ↔ (((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣)))))
37 eqtr2 2756 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑢)) = (2nd𝑢)) → (2nd𝑠) = (2nd𝑢))
3837ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (2nd𝑠) = (2nd𝑢))
39 eqtr2 2756 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍‘(1st𝑣)) = (2nd𝑟) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣)) → (2nd𝑟) = (2nd𝑣))
4039ad2ant2l 744 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (2nd𝑟) = (2nd𝑣))
4138, 40ineq12d 4212 . . . . . . . . . . . . . . . . . . . 20 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))
4236, 41syl6bi 252 . . . . . . . . . . . . . . . . . . 19 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣))))
4342com12 32 . . . . . . . . . . . . . . . . . 18 ((((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣))))
4443a1i 11 . . . . . . . . . . . . . . . . 17 (Fun 𝑍 → ((((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))))
4521, 26, 44syl2and 608 . . . . . . . . . . . . . . . 16 (Fun 𝑍 → (((𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))))
4645expd 416 . . . . . . . . . . . . . . 15 (Fun 𝑍 → ((𝑠𝑍𝑟𝑍) → ((𝑢𝑍𝑣𝑍) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣))))))
47463imp1 1347 . . . . . . . . . . . . . 14 (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))
4847difeq2d 4121 . . . . . . . . . . . . 13 (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) → ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
4948adantr 481 . . . . . . . . . . . 12 ((((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) ∧ (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
50 eqeq12 2749 . . . . . . . . . . . . 13 ((𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
5150adantl 482 . . . . . . . . . . . 12 ((((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) ∧ (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → (𝑦 = 𝑤 ↔ ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
5249, 51mpbird 256 . . . . . . . . . . 11 ((((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) ∧ (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → 𝑦 = 𝑤)
5352exp43 437 . . . . . . . . . 10 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) → 𝑦 = 𝑤))))
5453adantld 491 . . . . . . . . 9 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → ((1o = 1o ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) → 𝑦 = 𝑤))))
5516, 54biimtrid 241 . . . . . . . 8 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) → 𝑦 = 𝑤))))
561, 55syl5 34 . . . . . . 7 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) → 𝑦 = 𝑤))))
5756expd 416 . . . . . 6 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) → 𝑦 = 𝑤)))))
5857com35 98 . . . . 5 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → (𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → 𝑦 = 𝑤)))))
5958impd 411 . . . 4 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → 𝑦 = 𝑤))))
6059com24 95 . . 3 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → 𝑦 = 𝑤))))
6160impd 411 . 2 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → 𝑦 = 𝑤)))
62613imp 1111 1 (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → 𝑦 = 𝑤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  Vcvv 3474  cdif 3944  cin 3946  cop 4633  Fun wfun 6534  cfv 6540  (class class class)co 7405  ωcom 7851  1st c1st 7969  2nd c2nd 7970  1oc1o 8455  m cmap 8816  𝑔cgna 34313
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 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-suc 6367  df-iota 6492  df-fun 6542  df-fv 6548  df-ov 7408  df-1st 7971  df-2nd 7972  df-1o 8462  df-gona 34320
This theorem is referenced by:  satffunlem1lem1  34381  satffunlem2lem1  34383
  Copyright terms: Public domain W3C validator