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

Theorem goalr 32930
Description: If the "Godel-set of universal quantification" applied to a class is a Godel formula, the class is also a Godel formula. Remark: The reverse is not valid for 𝐴 being of the same height as the "Godel-set of universal quantification". (Contributed by AV, 22-Oct-2023.)
Assertion
Ref Expression
goalr ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → 𝑎 ∈ (Fmla‘𝑁))
Distinct variable groups:   𝑖,𝑁   𝑖,𝑎
Allowed substitution hint:   𝑁(𝑎)

Proof of Theorem goalr
Dummy variables 𝑗 𝑥 𝑘 𝑢 𝑣 𝑛 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 goaln0 32926 . . 3 (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅)
21adantl 485 . 2 ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → 𝑁 ≠ ∅)
3 nnsuc 7616 . . . 4 ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → ∃𝑛 ∈ ω 𝑁 = suc 𝑛)
4 suceq 6237 . . . . . . . . . . 11 (𝑥 = ∅ → suc 𝑥 = suc ∅)
54fveq2d 6678 . . . . . . . . . 10 (𝑥 = ∅ → (Fmla‘suc 𝑥) = (Fmla‘suc ∅))
65eleq2d 2818 . . . . . . . . 9 (𝑥 = ∅ → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅)))
75eleq2d 2818 . . . . . . . . 9 (𝑥 = ∅ → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc ∅)))
86, 7imbi12d 348 . . . . . . . 8 (𝑥 = ∅ → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) → 𝑎 ∈ (Fmla‘suc ∅))))
9 suceq 6237 . . . . . . . . . . 11 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
109fveq2d 6678 . . . . . . . . . 10 (𝑥 = 𝑦 → (Fmla‘suc 𝑥) = (Fmla‘suc 𝑦))
1110eleq2d 2818 . . . . . . . . 9 (𝑥 = 𝑦 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦)))
1210eleq2d 2818 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc 𝑦)))
1311, 12imbi12d 348 . . . . . . . 8 (𝑥 = 𝑦 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦) → 𝑎 ∈ (Fmla‘suc 𝑦))))
14 suceq 6237 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
1514fveq2d 6678 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (Fmla‘suc 𝑥) = (Fmla‘suc suc 𝑦))
1615eleq2d 2818 . . . . . . . . 9 (𝑥 = suc 𝑦 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦)))
1715eleq2d 2818 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc suc 𝑦)))
1816, 17imbi12d 348 . . . . . . . 8 (𝑥 = suc 𝑦 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦) → 𝑎 ∈ (Fmla‘suc suc 𝑦))))
19 suceq 6237 . . . . . . . . . . 11 (𝑥 = 𝑛 → suc 𝑥 = suc 𝑛)
2019fveq2d 6678 . . . . . . . . . 10 (𝑥 = 𝑛 → (Fmla‘suc 𝑥) = (Fmla‘suc 𝑛))
2120eleq2d 2818 . . . . . . . . 9 (𝑥 = 𝑛 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛)))
2220eleq2d 2818 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc 𝑛)))
2321, 22imbi12d 348 . . . . . . . 8 (𝑥 = 𝑛 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛))))
24 peano1 7620 . . . . . . . . . 10 ∅ ∈ ω
25 df-goal 32875 . . . . . . . . . . 11 𝑔𝑖𝑎 = ⟨2o, ⟨𝑖, 𝑎⟩⟩
26 opex 5322 . . . . . . . . . . 11 ⟨2o, ⟨𝑖, 𝑎⟩⟩ ∈ V
2725, 26eqeltri 2829 . . . . . . . . . 10 𝑔𝑖𝑎 ∈ V
28 isfmlasuc 32921 . . . . . . . . . 10 ((∅ ∈ ω ∧ ∀𝑔𝑖𝑎 ∈ V) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) ∨ ∃𝑘 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢))))
2924, 27, 28mp2an 692 . . . . . . . . 9 (∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) ∨ ∃𝑘 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢)))
30 eqeq1 2742 . . . . . . . . . . . . 13 (𝑥 = ∀𝑔𝑖𝑎 → (𝑥 = (𝑘𝑔𝑗) ↔ ∀𝑔𝑖𝑎 = (𝑘𝑔𝑗)))
31302rexbidv 3210 . . . . . . . . . . . 12 (𝑥 = ∀𝑔𝑖𝑎 → (∃𝑘 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑘𝑔𝑗) ↔ ∃𝑘 ∈ ω ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = (𝑘𝑔𝑗)))
32 fmla0 32915 . . . . . . . . . . . 12 (Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑘 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑘𝑔𝑗)}
3331, 32elrab2 3591 . . . . . . . . . . 11 (∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ↔ (∀𝑔𝑖𝑎 ∈ V ∧ ∃𝑘 ∈ ω ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = (𝑘𝑔𝑗)))
3425a1i 11 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) → ∀𝑔𝑖𝑎 = ⟨2o, ⟨𝑖, 𝑎⟩⟩)
35 goel 32880 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) → (𝑘𝑔𝑗) = ⟨∅, ⟨𝑘, 𝑗⟩⟩)
3634, 35eqeq12d 2754 . . . . . . . . . . . . . 14 ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) → (∀𝑔𝑖𝑎 = (𝑘𝑔𝑗) ↔ ⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨∅, ⟨𝑘, 𝑗⟩⟩))
37 2oex 8148 . . . . . . . . . . . . . . . 16 2o ∈ V
38 opex 5322 . . . . . . . . . . . . . . . 16 𝑖, 𝑎⟩ ∈ V
3937, 38opth 5334 . . . . . . . . . . . . . . 15 (⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨∅, ⟨𝑘, 𝑗⟩⟩ ↔ (2o = ∅ ∧ ⟨𝑖, 𝑎⟩ = ⟨𝑘, 𝑗⟩))
40 2on0 8140 . . . . . . . . . . . . . . . . 17 2o ≠ ∅
41 eqneqall 2945 . . . . . . . . . . . . . . . . 17 (2o = ∅ → (2o ≠ ∅ → 𝑎 ∈ (Fmla‘suc ∅)))
4240, 41mpi 20 . . . . . . . . . . . . . . . 16 (2o = ∅ → 𝑎 ∈ (Fmla‘suc ∅))
4342adantr 484 . . . . . . . . . . . . . . 15 ((2o = ∅ ∧ ⟨𝑖, 𝑎⟩ = ⟨𝑘, 𝑗⟩) → 𝑎 ∈ (Fmla‘suc ∅))
4439, 43sylbi 220 . . . . . . . . . . . . . 14 (⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨∅, ⟨𝑘, 𝑗⟩⟩ → 𝑎 ∈ (Fmla‘suc ∅))
4536, 44syl6bi 256 . . . . . . . . . . . . 13 ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) → (∀𝑔𝑖𝑎 = (𝑘𝑔𝑗) → 𝑎 ∈ (Fmla‘suc ∅)))
4645rexlimdva 3194 . . . . . . . . . . . 12 (𝑘 ∈ ω → (∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = (𝑘𝑔𝑗) → 𝑎 ∈ (Fmla‘suc ∅)))
4746rexlimiv 3190 . . . . . . . . . . 11 (∃𝑘 ∈ ω ∃𝑗 ∈ ω ∀𝑔𝑖𝑎 = (𝑘𝑔𝑗) → 𝑎 ∈ (Fmla‘suc ∅))
4833, 47simplbiim 508 . . . . . . . . . 10 (∀𝑔𝑖𝑎 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc ∅))
49 gonanegoal 32885 . . . . . . . . . . . . . . . 16 (𝑢𝑔𝑣) ≠ ∀𝑔𝑖𝑎
50 eqneqall 2945 . . . . . . . . . . . . . . . 16 ((𝑢𝑔𝑣) = ∀𝑔𝑖𝑎 → ((𝑢𝑔𝑣) ≠ ∀𝑔𝑖𝑎𝑎 ∈ (Fmla‘suc ∅)))
5149, 50mpi 20 . . . . . . . . . . . . . . 15 ((𝑢𝑔𝑣) = ∀𝑔𝑖𝑎𝑎 ∈ (Fmla‘suc ∅))
5251eqcoms 2746 . . . . . . . . . . . . . 14 (∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) → 𝑎 ∈ (Fmla‘suc ∅))
5352a1i 11 . . . . . . . . . . . . 13 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅)) → (∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) → 𝑎 ∈ (Fmla‘suc ∅)))
5453rexlimdva 3194 . . . . . . . . . . . 12 (𝑢 ∈ (Fmla‘∅) → (∃𝑣 ∈ (Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) → 𝑎 ∈ (Fmla‘suc ∅)))
55 df-goal 32875 . . . . . . . . . . . . . . 15 𝑔𝑘𝑢 = ⟨2o, ⟨𝑘, 𝑢⟩⟩
5625, 55eqeq12i 2753 . . . . . . . . . . . . . 14 (∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢 ↔ ⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨2o, ⟨𝑘, 𝑢⟩⟩)
5737, 38opth 5334 . . . . . . . . . . . . . . . . 17 (⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨2o, ⟨𝑘, 𝑢⟩⟩ ↔ (2o = 2o ∧ ⟨𝑖, 𝑎⟩ = ⟨𝑘, 𝑢⟩))
58 vex 3402 . . . . . . . . . . . . . . . . . . 19 𝑖 ∈ V
59 vex 3402 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ V
6058, 59opth 5334 . . . . . . . . . . . . . . . . . 18 (⟨𝑖, 𝑎⟩ = ⟨𝑘, 𝑢⟩ ↔ (𝑖 = 𝑘𝑎 = 𝑢))
61 eleq1w 2815 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘∅) ↔ 𝑎 ∈ (Fmla‘∅)))
62 fmlasssuc 32922 . . . . . . . . . . . . . . . . . . . . . 22 (∅ ∈ ω → (Fmla‘∅) ⊆ (Fmla‘suc ∅))
6324, 62ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (Fmla‘∅) ⊆ (Fmla‘suc ∅)
6463sseli 3873 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc ∅))
6561, 64syl6bi 256 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc ∅)))
6665eqcoms 2746 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc ∅)))
6760, 66simplbiim 508 . . . . . . . . . . . . . . . . 17 (⟨𝑖, 𝑎⟩ = ⟨𝑘, 𝑢⟩ → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc ∅)))
6857, 67simplbiim 508 . . . . . . . . . . . . . . . 16 (⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨2o, ⟨𝑘, 𝑢⟩⟩ → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc ∅)))
6968com12 32 . . . . . . . . . . . . . . 15 (𝑢 ∈ (Fmla‘∅) → (⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨2o, ⟨𝑘, 𝑢⟩⟩ → 𝑎 ∈ (Fmla‘suc ∅)))
7069adantr 484 . . . . . . . . . . . . . 14 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑘 ∈ ω) → (⟨2o, ⟨𝑖, 𝑎⟩⟩ = ⟨2o, ⟨𝑘, 𝑢⟩⟩ → 𝑎 ∈ (Fmla‘suc ∅)))
7156, 70syl5bi 245 . . . . . . . . . . . . 13 ((𝑢 ∈ (Fmla‘∅) ∧ 𝑘 ∈ ω) → (∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢𝑎 ∈ (Fmla‘suc ∅)))
7271rexlimdva 3194 . . . . . . . . . . . 12 (𝑢 ∈ (Fmla‘∅) → (∃𝑘 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢𝑎 ∈ (Fmla‘suc ∅)))
7354, 72jaod 858 . . . . . . . . . . 11 (𝑢 ∈ (Fmla‘∅) → ((∃𝑣 ∈ (Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) ∨ ∃𝑘 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢) → 𝑎 ∈ (Fmla‘suc ∅)))
7473rexlimiv 3190 . . . . . . . . . 10 (∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) ∨ ∃𝑘 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢) → 𝑎 ∈ (Fmla‘suc ∅))
7548, 74jaoi 856 . . . . . . . . 9 ((∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢𝑔𝑣) ∨ ∃𝑘 ∈ ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢)) → 𝑎 ∈ (Fmla‘suc ∅))
7629, 75sylbi 220 . . . . . . . 8 (∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) → 𝑎 ∈ (Fmla‘suc ∅))
77 goalrlem 32929 . . . . . . . 8 (𝑦 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦) → 𝑎 ∈ (Fmla‘suc 𝑦)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦) → 𝑎 ∈ (Fmla‘suc suc 𝑦))))
788, 13, 18, 23, 76, 77finds 7629 . . . . . . 7 (𝑛 ∈ ω → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))
7978adantr 484 . . . . . 6 ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))
80 fveq2 6674 . . . . . . . . 9 (𝑁 = suc 𝑛 → (Fmla‘𝑁) = (Fmla‘suc 𝑛))
8180eleq2d 2818 . . . . . . . 8 (𝑁 = suc 𝑛 → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛)))
8280eleq2d 2818 . . . . . . . 8 (𝑁 = suc 𝑛 → (𝑎 ∈ (Fmla‘𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑛)))
8381, 82imbi12d 348 . . . . . . 7 (𝑁 = suc 𝑛 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛))))
8483adantl 485 . . . . . 6 ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → ((∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛))))
8579, 84mpbird 260 . . . . 5 ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)))
8685rexlimiva 3191 . . . 4 (∃𝑛 ∈ ω 𝑁 = suc 𝑛 → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)))
873, 86syl 17 . . 3 ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)))
8887impancom 455 . 2 ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → (𝑁 ≠ ∅ → 𝑎 ∈ (Fmla‘𝑁)))
892, 88mpd 15 1 ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → 𝑎 ∈ (Fmla‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 846   = wceq 1542  wcel 2114  wne 2934  wrex 3054  Vcvv 3398  wss 3843  c0 4211  cop 4522  suc csuc 6174  cfv 6339  (class class class)co 7170  ωcom 7599  2oc2o 8125  𝑔cgoe 32866  𝑔cgna 32867  𝑔cgol 32868  Fmlacfmla 32870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-inf2 9177
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-2o 8132  df-map 8439  df-goel 32873  df-gona 32874  df-goal 32875  df-sat 32876  df-fmla 32878
This theorem is referenced by:  fmlasucdisj  32932
  Copyright terms: Public domain W3C validator