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 34881
Description: Lemma for satffunlem1lem1 34882 and satffunlem2lem1 34884. (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 2748 . . . . . . . 8 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)))
2 fvex 6894 . . . . . . . . . . . 12 (1st𝑢) ∈ V
3 fvex 6894 . . . . . . . . . . . 12 (1st𝑣) ∈ V
4 gonafv 34830 . . . . . . . . . . . 12 (((1st𝑢) ∈ V ∧ (1st𝑣) ∈ V) → ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
52, 3, 4mp2an 689 . . . . . . . . . . 11 ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩
6 fvex 6894 . . . . . . . . . . . 12 (1st𝑠) ∈ V
7 fvex 6894 . . . . . . . . . . . 12 (1st𝑟) ∈ V
8 gonafv 34830 . . . . . . . . . . . 12 (((1st𝑠) ∈ V ∧ (1st𝑟) ∈ V) → ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
96, 7, 8mp2an 689 . . . . . . . . . . 11 ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩
105, 9eqeq12i 2742 . . . . . . . . . 10 (((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)) ↔ ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
11 1oex 8471 . . . . . . . . . . 11 1o ∈ V
12 opex 5454 . . . . . . . . . . 11 ⟨(1st𝑢), (1st𝑣)⟩ ∈ V
1311, 12opth 5466 . . . . . . . . . 10 (⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ ↔ (1o = 1o ∧ ⟨(1st𝑢), (1st𝑣)⟩ = ⟨(1st𝑠), (1st𝑟)⟩))
142, 3opth 5466 . . . . . . . . . . 11 (⟨(1st𝑢), (1st𝑣)⟩ = ⟨(1st𝑠), (1st𝑟)⟩ ↔ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)))
1514anbi2i 622 . . . . . . . . . 10 ((1o = 1o ∧ ⟨(1st𝑢), (1st𝑣)⟩ = ⟨(1st𝑠), (1st𝑟)⟩) ↔ (1o = 1o ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))))
1610, 13, 153bitri 297 . . . . . . . . 9 (((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)) ↔ (1o = 1o ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))))
17 funfv1st2nd 8025 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑠𝑍) → (𝑍‘(1st𝑠)) = (2nd𝑠))
1817ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑠𝑍 → (𝑍‘(1st𝑠)) = (2nd𝑠)))
19 funfv1st2nd 8025 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑟𝑍) → (𝑍‘(1st𝑟)) = (2nd𝑟))
2019ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑟𝑍 → (𝑍‘(1st𝑟)) = (2nd𝑟)))
2118, 20anim12d 608 . . . . . . . . . . . . . . . . 17 (Fun 𝑍 → ((𝑠𝑍𝑟𝑍) → ((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟))))
22 funfv1st2nd 8025 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑢𝑍) → (𝑍‘(1st𝑢)) = (2nd𝑢))
2322ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑢𝑍 → (𝑍‘(1st𝑢)) = (2nd𝑢)))
24 funfv1st2nd 8025 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑣𝑍) → (𝑍‘(1st𝑣)) = (2nd𝑣))
2524ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑣𝑍 → (𝑍‘(1st𝑣)) = (2nd𝑣)))
2623, 25anim12d 608 . . . . . . . . . . . . . . . . 17 (Fun 𝑍 → ((𝑢𝑍𝑣𝑍) → ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))))
27 fveq2 6881 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) = (1st𝑢) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
2827eqcoms 2732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑢) = (1st𝑠) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
2928adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
3029eqeq1d 2726 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((𝑍‘(1st𝑠)) = (2nd𝑠) ↔ (𝑍‘(1st𝑢)) = (2nd𝑠)))
31 fveq2 6881 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑟) = (1st𝑣) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3231eqcoms 2732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑣) = (1st𝑟) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3332adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3433eqeq1d 2726 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((𝑍‘(1st𝑟)) = (2nd𝑟) ↔ (𝑍‘(1st𝑣)) = (2nd𝑟)))
3530, 34anbi12d 630 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ↔ ((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟))))
3635anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) ↔ (((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣)))))
37 eqtr2 2748 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑢)) = (2nd𝑢)) → (2nd𝑠) = (2nd𝑢))
3837ad2ant2r 744 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (2nd𝑠) = (2nd𝑢))
39 eqtr2 2748 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍‘(1st𝑣)) = (2nd𝑟) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣)) → (2nd𝑟) = (2nd𝑣))
4039ad2ant2l 743 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (2nd𝑟) = (2nd𝑣))
4138, 40ineq12d 4205 . . . . . . . . . . . . . . . . . . . 20 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))
4236, 41syl6bi 253 . . . . . . . . . . . . . . . . . . 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 607 . . . . . . . . . . . . . . . 16 (Fun 𝑍 → (((𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))))
4645expd 415 . . . . . . . . . . . . . . 15 (Fun 𝑍 → ((𝑠𝑍𝑟𝑍) → ((𝑢𝑍𝑣𝑍) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣))))))
47463imp1 1344 . . . . . . . . . . . . . 14 (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))
4847difeq2d 4114 . . . . . . . . . . . . 13 (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) → ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
4948adantr 480 . . . . . . . . . . . 12 ((((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) ∧ (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
50 eqeq12 2741 . . . . . . . . . . . . 13 ((𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
5150adantl 481 . . . . . . . . . . . 12 ((((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) ∧ (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → (𝑦 = 𝑤 ↔ ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))))
5249, 51mpbird 257 . . . . . . . . . . 11 ((((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) ∧ (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → 𝑦 = 𝑤)
5352exp43 436 . . . . . . . . . 10 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟))) → (𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))) → 𝑦 = 𝑤))))
5453adantld 490 . . . . . . . . 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 415 . . . . . 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 410 . . . 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 410 . 2 ((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → ((𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) → ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) → 𝑦 = 𝑤)))
62613imp 1108 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 395  w3a 1084   = wceq 1533  wcel 2098  Vcvv 3466  cdif 3937  cin 3939  cop 4626  Fun wfun 6527  cfv 6533  (class class class)co 7401  ωcom 7848  1st c1st 7966  2nd c2nd 7967  1oc1o 8454  m cmap 8816  𝑔cgna 34814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-suc 6360  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7404  df-1st 7968  df-2nd 7969  df-1o 8461  df-gona 34821
This theorem is referenced by:  satffunlem1lem1  34882  satffunlem2lem1  34884
  Copyright terms: Public domain W3C validator