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 35385
Description: Lemma for satffunlem1lem1 35386 and satffunlem2lem1 35388. (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 2758 . . . . . . . 8 ((𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑥 = ((1st𝑠)⊼𝑔(1st𝑟))) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)))
2 fvex 6919 . . . . . . . . . . . 12 (1st𝑢) ∈ V
3 fvex 6919 . . . . . . . . . . . 12 (1st𝑣) ∈ V
4 gonafv 35334 . . . . . . . . . . . 12 (((1st𝑢) ∈ V ∧ (1st𝑣) ∈ V) → ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩)
52, 3, 4mp2an 692 . . . . . . . . . . 11 ((1st𝑢)⊼𝑔(1st𝑣)) = ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩
6 fvex 6919 . . . . . . . . . . . 12 (1st𝑠) ∈ V
7 fvex 6919 . . . . . . . . . . . 12 (1st𝑟) ∈ V
8 gonafv 35334 . . . . . . . . . . . 12 (((1st𝑠) ∈ V ∧ (1st𝑟) ∈ V) → ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
96, 7, 8mp2an 692 . . . . . . . . . . 11 ((1st𝑠)⊼𝑔(1st𝑟)) = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩
105, 9eqeq12i 2752 . . . . . . . . . 10 (((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)) ↔ ⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩)
11 1oex 8514 . . . . . . . . . . 11 1o ∈ V
12 opex 5474 . . . . . . . . . . 11 ⟨(1st𝑢), (1st𝑣)⟩ ∈ V
1311, 12opth 5486 . . . . . . . . . 10 (⟨1o, ⟨(1st𝑢), (1st𝑣)⟩⟩ = ⟨1o, ⟨(1st𝑠), (1st𝑟)⟩⟩ ↔ (1o = 1o ∧ ⟨(1st𝑢), (1st𝑣)⟩ = ⟨(1st𝑠), (1st𝑟)⟩))
142, 3opth 5486 . . . . . . . . . . 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 297 . . . . . . . . 9 (((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑠)⊼𝑔(1st𝑟)) ↔ (1o = 1o ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))))
17 funfv1st2nd 8069 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑠𝑍) → (𝑍‘(1st𝑠)) = (2nd𝑠))
1817ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑠𝑍 → (𝑍‘(1st𝑠)) = (2nd𝑠)))
19 funfv1st2nd 8069 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑟𝑍) → (𝑍‘(1st𝑟)) = (2nd𝑟))
2019ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑟𝑍 → (𝑍‘(1st𝑟)) = (2nd𝑟)))
2118, 20anim12d 609 . . . . . . . . . . . . . . . . 17 (Fun 𝑍 → ((𝑠𝑍𝑟𝑍) → ((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟))))
22 funfv1st2nd 8069 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑢𝑍) → (𝑍‘(1st𝑢)) = (2nd𝑢))
2322ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑢𝑍 → (𝑍‘(1st𝑢)) = (2nd𝑢)))
24 funfv1st2nd 8069 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑍𝑣𝑍) → (𝑍‘(1st𝑣)) = (2nd𝑣))
2524ex 412 . . . . . . . . . . . . . . . . . 18 (Fun 𝑍 → (𝑣𝑍 → (𝑍‘(1st𝑣)) = (2nd𝑣)))
2623, 25anim12d 609 . . . . . . . . . . . . . . . . 17 (Fun 𝑍 → ((𝑢𝑍𝑣𝑍) → ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))))
27 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) = (1st𝑢) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
2827eqcoms 2742 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑢) = (1st𝑠) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
2928adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑍‘(1st𝑠)) = (𝑍‘(1st𝑢)))
3029eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((𝑍‘(1st𝑠)) = (2nd𝑠) ↔ (𝑍‘(1st𝑢)) = (2nd𝑠)))
31 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑟) = (1st𝑣) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3231eqcoms 2742 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑣) = (1st𝑟) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3332adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (𝑍‘(1st𝑟)) = (𝑍‘(1st𝑣)))
3433eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . 22 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((𝑍‘(1st𝑟)) = (2nd𝑟) ↔ (𝑍‘(1st𝑣)) = (2nd𝑟)))
3530, 34anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → (((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ↔ ((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟))))
3635anbi1d 631 . . . . . . . . . . . . . . . . . . . 20 (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((((𝑍‘(1st𝑠)) = (2nd𝑠) ∧ (𝑍‘(1st𝑟)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) ↔ (((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣)))))
37 eqtr2 2758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑢)) = (2nd𝑢)) → (2nd𝑠) = (2nd𝑢))
3837ad2ant2r 747 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (2nd𝑠) = (2nd𝑢))
39 eqtr2 2758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍‘(1st𝑣)) = (2nd𝑟) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣)) → (2nd𝑟) = (2nd𝑣))
4039ad2ant2l 746 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → (2nd𝑟) = (2nd𝑣))
4138, 40ineq12d 4228 . . . . . . . . . . . . . . . . . . . 20 ((((𝑍‘(1st𝑢)) = (2nd𝑠) ∧ (𝑍‘(1st𝑣)) = (2nd𝑟)) ∧ ((𝑍‘(1st𝑢)) = (2nd𝑢) ∧ (𝑍‘(1st𝑣)) = (2nd𝑣))) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))
4236, 41biimtrdi 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 608 . . . . . . . . . . . . . . . 16 (Fun 𝑍 → (((𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))))
4645expd 415 . . . . . . . . . . . . . . 15 (Fun 𝑍 → ((𝑠𝑍𝑟𝑍) → ((𝑢𝑍𝑣𝑍) → (((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟)) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣))))))
47463imp1 1346 . . . . . . . . . . . . . 14 (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ ((1st𝑢) = (1st𝑠) ∧ (1st𝑣) = (1st𝑟))) → ((2nd𝑠) ∩ (2nd𝑟)) = ((2nd𝑢) ∩ (2nd𝑣)))
4847difeq2d 4135 . . . . . . . . . . . . 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 2751 . . . . . . . . . . . . 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 242 . . . . . . . 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 1110 1 (((Fun 𝑍 ∧ (𝑠𝑍𝑟𝑍) ∧ (𝑢𝑍𝑣𝑍)) ∧ (𝑥 = ((1st𝑠)⊼𝑔(1st𝑟)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑠) ∩ (2nd𝑟)))) ∧ (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑤 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))) → 𝑦 = 𝑤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  Vcvv 3477  cdif 3959  cin 3961  cop 4636  Fun wfun 6556  cfv 6562  (class class class)co 7430  ωcom 7886  1st c1st 8010  2nd c2nd 8011  1oc1o 8497  m cmap 8864  𝑔cgna 35318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-suc 6391  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-1st 8012  df-2nd 8013  df-1o 8504  df-gona 35325
This theorem is referenced by:  satffunlem1lem1  35386  satffunlem2lem1  35388
  Copyright terms: Public domain W3C validator