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 34852
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 34848 . . 3 (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘) β†’ 𝑁 β‰  βˆ…)
21adantl 481 . 2 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ 𝑁 β‰  βˆ…)
3 nnsuc 7877 . . . 4 ((𝑁 ∈ Ο‰ ∧ 𝑁 β‰  βˆ…) β†’ βˆƒπ‘› ∈ Ο‰ 𝑁 = suc 𝑛)
4 suceq 6430 . . . . . . . . . . 11 (π‘₯ = βˆ… β†’ suc π‘₯ = suc βˆ…)
54fveq2d 6895 . . . . . . . . . 10 (π‘₯ = βˆ… β†’ (Fmlaβ€˜suc π‘₯) = (Fmlaβ€˜suc βˆ…))
65eleq2d 2818 . . . . . . . . 9 (π‘₯ = βˆ… β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc π‘₯) ↔ βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
75eleq2d 2818 . . . . . . . . 9 (π‘₯ = βˆ… β†’ (π‘Ž ∈ (Fmlaβ€˜suc π‘₯) ↔ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
86, 7imbi12d 344 . . . . . . . 8 (π‘₯ = βˆ… β†’ ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc π‘₯) β†’ π‘Ž ∈ (Fmlaβ€˜suc π‘₯)) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))))
9 suceq 6430 . . . . . . . . . . 11 (π‘₯ = 𝑦 β†’ suc π‘₯ = suc 𝑦)
109fveq2d 6895 . . . . . . . . . 10 (π‘₯ = 𝑦 β†’ (Fmlaβ€˜suc π‘₯) = (Fmlaβ€˜suc 𝑦))
1110eleq2d 2818 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc π‘₯) ↔ βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑦)))
1210eleq2d 2818 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (π‘Ž ∈ (Fmlaβ€˜suc π‘₯) ↔ π‘Ž ∈ (Fmlaβ€˜suc 𝑦)))
1311, 12imbi12d 344 . . . . . . . 8 (π‘₯ = 𝑦 β†’ ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc π‘₯) β†’ π‘Ž ∈ (Fmlaβ€˜suc π‘₯)) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑦) β†’ π‘Ž ∈ (Fmlaβ€˜suc 𝑦))))
14 suceq 6430 . . . . . . . . . . 11 (π‘₯ = suc 𝑦 β†’ suc π‘₯ = suc suc 𝑦)
1514fveq2d 6895 . . . . . . . . . 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 344 . . . . . . . 8 (π‘₯ = suc 𝑦 β†’ ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc π‘₯) β†’ π‘Ž ∈ (Fmlaβ€˜suc π‘₯)) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc suc 𝑦) β†’ π‘Ž ∈ (Fmlaβ€˜suc suc 𝑦))))
19 suceq 6430 . . . . . . . . . . 11 (π‘₯ = 𝑛 β†’ suc π‘₯ = suc 𝑛)
2019fveq2d 6895 . . . . . . . . . 10 (π‘₯ = 𝑛 β†’ (Fmlaβ€˜suc π‘₯) = (Fmlaβ€˜suc 𝑛))
2120eleq2d 2818 . . . . . . . . 9 (π‘₯ = 𝑛 β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc π‘₯) ↔ βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑛)))
2220eleq2d 2818 . . . . . . . . 9 (π‘₯ = 𝑛 β†’ (π‘Ž ∈ (Fmlaβ€˜suc π‘₯) ↔ π‘Ž ∈ (Fmlaβ€˜suc 𝑛)))
2321, 22imbi12d 344 . . . . . . . 8 (π‘₯ = 𝑛 β†’ ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc π‘₯) β†’ π‘Ž ∈ (Fmlaβ€˜suc π‘₯)) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑛) β†’ π‘Ž ∈ (Fmlaβ€˜suc 𝑛))))
24 peano1 7883 . . . . . . . . . 10 βˆ… ∈ Ο‰
25 df-goal 34797 . . . . . . . . . . 11 βˆ€π‘”π‘–π‘Ž = ⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ©
26 opex 5464 . . . . . . . . . . 11 ⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© ∈ V
2725, 26eqeltri 2828 . . . . . . . . . 10 βˆ€π‘”π‘–π‘Ž ∈ V
28 isfmlasuc 34843 . . . . . . . . . 10 ((βˆ… ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘Ž ∈ V) β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc βˆ…) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜βˆ…) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘£ ∈ (Fmlaβ€˜βˆ…)βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’))))
2924, 27, 28mp2an 689 . . . . . . . . 9 (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc βˆ…) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜βˆ…) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘£ ∈ (Fmlaβ€˜βˆ…)βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’)))
30 eqeq1 2735 . . . . . . . . . . . . 13 (π‘₯ = βˆ€π‘”π‘–π‘Ž β†’ (π‘₯ = (π‘˜βˆˆπ‘”π‘—) ↔ βˆ€π‘”π‘–π‘Ž = (π‘˜βˆˆπ‘”π‘—)))
31302rexbidv 3218 . . . . . . . . . . . 12 (π‘₯ = βˆ€π‘”π‘–π‘Ž β†’ (βˆƒπ‘˜ ∈ Ο‰ βˆƒπ‘— ∈ Ο‰ π‘₯ = (π‘˜βˆˆπ‘”π‘—) ↔ βˆƒπ‘˜ ∈ Ο‰ βˆƒπ‘— ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = (π‘˜βˆˆπ‘”π‘—)))
32 fmla0 34837 . . . . . . . . . . . 12 (Fmlaβ€˜βˆ…) = {π‘₯ ∈ V ∣ βˆƒπ‘˜ ∈ Ο‰ βˆƒπ‘— ∈ Ο‰ π‘₯ = (π‘˜βˆˆπ‘”π‘—)}
3331, 32elrab2 3686 . . . . . . . . . . 11 (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜βˆ…) ↔ (βˆ€π‘”π‘–π‘Ž ∈ V ∧ βˆƒπ‘˜ ∈ Ο‰ βˆƒπ‘— ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = (π‘˜βˆˆπ‘”π‘—)))
3425a1i 11 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ Ο‰ ∧ 𝑗 ∈ Ο‰) β†’ βˆ€π‘”π‘–π‘Ž = ⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ©)
35 goel 34802 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ Ο‰ ∧ 𝑗 ∈ Ο‰) β†’ (π‘˜βˆˆπ‘”π‘—) = βŸ¨βˆ…, βŸ¨π‘˜, π‘—βŸ©βŸ©)
3634, 35eqeq12d 2747 . . . . . . . . . . . . . 14 ((π‘˜ ∈ Ο‰ ∧ 𝑗 ∈ Ο‰) β†’ (βˆ€π‘”π‘–π‘Ž = (π‘˜βˆˆπ‘”π‘—) ↔ ⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = βŸ¨βˆ…, βŸ¨π‘˜, π‘—βŸ©βŸ©))
37 2oex 8483 . . . . . . . . . . . . . . . 16 2o ∈ V
38 opex 5464 . . . . . . . . . . . . . . . 16 βŸ¨π‘–, π‘ŽβŸ© ∈ V
3937, 38opth 5476 . . . . . . . . . . . . . . 15 (⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = βŸ¨βˆ…, βŸ¨π‘˜, π‘—βŸ©βŸ© ↔ (2o = βˆ… ∧ βŸ¨π‘–, π‘ŽβŸ© = βŸ¨π‘˜, π‘—βŸ©))
40 2on0 8488 . . . . . . . . . . . . . . . . 17 2o β‰  βˆ…
41 eqneqall 2950 . . . . . . . . . . . . . . . . 17 (2o = βˆ… β†’ (2o β‰  βˆ… β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
4240, 41mpi 20 . . . . . . . . . . . . . . . 16 (2o = βˆ… β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
4342adantr 480 . . . . . . . . . . . . . . 15 ((2o = βˆ… ∧ βŸ¨π‘–, π‘ŽβŸ© = βŸ¨π‘˜, π‘—βŸ©) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
4439, 43sylbi 216 . . . . . . . . . . . . . 14 (⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = βŸ¨βˆ…, βŸ¨π‘˜, π‘—βŸ©βŸ© β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
4536, 44syl6bi 253 . . . . . . . . . . . . 13 ((π‘˜ ∈ Ο‰ ∧ 𝑗 ∈ Ο‰) β†’ (βˆ€π‘”π‘–π‘Ž = (π‘˜βˆˆπ‘”π‘—) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
4645rexlimdva 3154 . . . . . . . . . . . 12 (π‘˜ ∈ Ο‰ β†’ (βˆƒπ‘— ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = (π‘˜βˆˆπ‘”π‘—) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
4746rexlimiv 3147 . . . . . . . . . . 11 (βˆƒπ‘˜ ∈ Ο‰ βˆƒπ‘— ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = (π‘˜βˆˆπ‘”π‘—) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
4833, 47simplbiim 504 . . . . . . . . . 10 (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
49 gonanegoal 34807 . . . . . . . . . . . . . . . 16 (π‘’βŠΌπ‘”π‘£) β‰  βˆ€π‘”π‘–π‘Ž
50 eqneqall 2950 . . . . . . . . . . . . . . . 16 ((π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘–π‘Ž β†’ ((π‘’βŠΌπ‘”π‘£) β‰  βˆ€π‘”π‘–π‘Ž β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
5149, 50mpi 20 . . . . . . . . . . . . . . 15 ((π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘–π‘Ž β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
5251eqcoms 2739 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
5352a1i 11 . . . . . . . . . . . . 13 ((𝑒 ∈ (Fmlaβ€˜βˆ…) ∧ 𝑣 ∈ (Fmlaβ€˜βˆ…)) β†’ (βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
5453rexlimdva 3154 . . . . . . . . . . . 12 (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ (βˆƒπ‘£ ∈ (Fmlaβ€˜βˆ…)βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
55 df-goal 34797 . . . . . . . . . . . . . . 15 βˆ€π‘”π‘˜π‘’ = ⟨2o, βŸ¨π‘˜, π‘’βŸ©βŸ©
5625, 55eqeq12i 2749 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’ ↔ ⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = ⟨2o, βŸ¨π‘˜, π‘’βŸ©βŸ©)
5737, 38opth 5476 . . . . . . . . . . . . . . . . 17 (⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = ⟨2o, βŸ¨π‘˜, π‘’βŸ©βŸ© ↔ (2o = 2o ∧ βŸ¨π‘–, π‘ŽβŸ© = βŸ¨π‘˜, π‘’βŸ©))
58 vex 3477 . . . . . . . . . . . . . . . . . . 19 𝑖 ∈ V
59 vex 3477 . . . . . . . . . . . . . . . . . . 19 π‘Ž ∈ V
6058, 59opth 5476 . . . . . . . . . . . . . . . . . 18 (βŸ¨π‘–, π‘ŽβŸ© = βŸ¨π‘˜, π‘’βŸ© ↔ (𝑖 = π‘˜ ∧ π‘Ž = 𝑒))
61 eleq1w 2815 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = π‘Ž β†’ (𝑒 ∈ (Fmlaβ€˜βˆ…) ↔ π‘Ž ∈ (Fmlaβ€˜βˆ…)))
62 fmlasssuc 34844 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ… ∈ Ο‰ β†’ (Fmlaβ€˜βˆ…) βŠ† (Fmlaβ€˜suc βˆ…))
6324, 62ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (Fmlaβ€˜βˆ…) βŠ† (Fmlaβ€˜suc βˆ…)
6463sseli 3978 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž ∈ (Fmlaβ€˜βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
6561, 64syl6bi 253 . . . . . . . . . . . . . . . . . . 19 (𝑒 = π‘Ž β†’ (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
6665eqcoms 2739 . . . . . . . . . . . . . . . . . 18 (π‘Ž = 𝑒 β†’ (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
6760, 66simplbiim 504 . . . . . . . . . . . . . . . . 17 (βŸ¨π‘–, π‘ŽβŸ© = βŸ¨π‘˜, π‘’βŸ© β†’ (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
6857, 67simplbiim 504 . . . . . . . . . . . . . . . 16 (⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = ⟨2o, βŸ¨π‘˜, π‘’βŸ©βŸ© β†’ (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
6968com12 32 . . . . . . . . . . . . . . 15 (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ (⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = ⟨2o, βŸ¨π‘˜, π‘’βŸ©βŸ© β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
7069adantr 480 . . . . . . . . . . . . . 14 ((𝑒 ∈ (Fmlaβ€˜βˆ…) ∧ π‘˜ ∈ Ο‰) β†’ (⟨2o, βŸ¨π‘–, π‘ŽβŸ©βŸ© = ⟨2o, βŸ¨π‘˜, π‘’βŸ©βŸ© β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
7156, 70biimtrid 241 . . . . . . . . . . . . 13 ((𝑒 ∈ (Fmlaβ€˜βˆ…) ∧ π‘˜ ∈ Ο‰) β†’ (βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’ β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
7271rexlimdva 3154 . . . . . . . . . . . 12 (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ (βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’ β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
7354, 72jaod 856 . . . . . . . . . . 11 (𝑒 ∈ (Fmlaβ€˜βˆ…) β†’ ((βˆƒπ‘£ ∈ (Fmlaβ€˜βˆ…)βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…)))
7473rexlimiv 3147 . . . . . . . . . 10 (βˆƒπ‘’ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘£ ∈ (Fmlaβ€˜βˆ…)βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
7548, 74jaoi 854 . . . . . . . . 9 ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜βˆ…) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘£ ∈ (Fmlaβ€˜βˆ…)βˆ€π‘”π‘–π‘Ž = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘”π‘–π‘Ž = βˆ€π‘”π‘˜π‘’)) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
7629, 75sylbi 216 . . . . . . . 8 (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc βˆ…) β†’ π‘Ž ∈ (Fmlaβ€˜suc βˆ…))
77 goalrlem 34851 . . . . . . . 8 (𝑦 ∈ Ο‰ β†’ ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑦) β†’ π‘Ž ∈ (Fmlaβ€˜suc 𝑦)) β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc suc 𝑦) β†’ π‘Ž ∈ (Fmlaβ€˜suc suc 𝑦))))
788, 13, 18, 23, 76, 77finds 7893 . . . . . . 7 (𝑛 ∈ Ο‰ β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑛) β†’ π‘Ž ∈ (Fmlaβ€˜suc 𝑛)))
7978adantr 480 . . . . . 6 ((𝑛 ∈ Ο‰ ∧ 𝑁 = suc 𝑛) β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑛) β†’ π‘Ž ∈ (Fmlaβ€˜suc 𝑛)))
80 fveq2 6891 . . . . . . . . 9 (𝑁 = suc 𝑛 β†’ (Fmlaβ€˜π‘) = (Fmlaβ€˜suc 𝑛))
8180eleq2d 2818 . . . . . . . 8 (𝑁 = suc 𝑛 β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘) ↔ βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑛)))
8280eleq2d 2818 . . . . . . . 8 (𝑁 = suc 𝑛 β†’ (π‘Ž ∈ (Fmlaβ€˜π‘) ↔ π‘Ž ∈ (Fmlaβ€˜suc 𝑛)))
8381, 82imbi12d 344 . . . . . . 7 (𝑁 = suc 𝑛 β†’ ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘) β†’ π‘Ž ∈ (Fmlaβ€˜π‘)) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑛) β†’ π‘Ž ∈ (Fmlaβ€˜suc 𝑛))))
8483adantl 481 . . . . . 6 ((𝑛 ∈ Ο‰ ∧ 𝑁 = suc 𝑛) β†’ ((βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘) β†’ π‘Ž ∈ (Fmlaβ€˜π‘)) ↔ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜suc 𝑛) β†’ π‘Ž ∈ (Fmlaβ€˜suc 𝑛))))
8579, 84mpbird 257 . . . . 5 ((𝑛 ∈ Ο‰ ∧ 𝑁 = suc 𝑛) β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘) β†’ π‘Ž ∈ (Fmlaβ€˜π‘)))
8685rexlimiva 3146 . . . 4 (βˆƒπ‘› ∈ Ο‰ 𝑁 = suc 𝑛 β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘) β†’ π‘Ž ∈ (Fmlaβ€˜π‘)))
873, 86syl 17 . . 3 ((𝑁 ∈ Ο‰ ∧ 𝑁 β‰  βˆ…) β†’ (βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘) β†’ π‘Ž ∈ (Fmlaβ€˜π‘)))
8887impancom 451 . 2 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (𝑁 β‰  βˆ… β†’ π‘Ž ∈ (Fmlaβ€˜π‘)))
892, 88mpd 15 1 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ π‘Ž ∈ (Fmlaβ€˜π‘))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆƒwrex 3069  Vcvv 3473   βŠ† wss 3948  βˆ…c0 4322  βŸ¨cop 4634  suc csuc 6366  β€˜cfv 6543  (class class class)co 7412  Ο‰com 7859  2oc2o 8466  βˆˆπ‘”cgoe 34788  βŠΌπ‘”cgna 34789  βˆ€π‘”cgol 34790  Fmlacfmla 34792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9642
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-2o 8473  df-map 8828  df-goel 34795  df-gona 34796  df-goal 34797  df-sat 34798  df-fmla 34800
This theorem is referenced by:  fmlasucdisj  34854
  Copyright terms: Public domain W3C validator