Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmlasucdisj Structured version   Visualization version   GIF version
Theorem fmlasucdisj 34379
Description: The valid Godel formulas of height (𝑁 + 1) is disjoint with the difference ((Fmlaβ€˜suc suc 𝑁) βˆ– (Fmlaβ€˜suc 𝑁)), expressed by formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification based on the valid Godel formulas of height (𝑁 + 1). (Contributed by AV, 20-Oct-2023.)
Assertion
Ref Expression
fmlasucdisj (𝑁 ∈ Ο‰ β†’ ((Fmlaβ€˜suc 𝑁) ∩ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))}) = βˆ…)
Distinct variable group:   𝑖,𝑁,𝑒,𝑣,π‘₯
Proof of Theorem fmlasucdisj
Dummy variables π‘Ž 𝑏 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3479 . . . . 5 𝑓 ∈ V
2 eqeq1 2737 . . . . . . . . 9 (π‘₯ = 𝑓 β†’ (π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ 𝑓 = (π‘’βŠΌπ‘”π‘£)))
32rexbidv 3179 . . . . . . . 8 (π‘₯ = 𝑓 β†’ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£)))
4 eqeq1 2737 . . . . . . . . 9 (π‘₯ = 𝑓 β†’ (π‘₯ = βˆ€π‘”π‘–π‘’ ↔ 𝑓 = βˆ€π‘”π‘–π‘’))
54rexbidv 3179 . . . . . . . 8 (π‘₯ = 𝑓 β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’ ↔ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’))
63, 5orbi12d 918 . . . . . . 7 (π‘₯ = 𝑓 β†’ ((βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ↔ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’)))
76rexbidv 3179 . . . . . 6 (π‘₯ = 𝑓 β†’ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ↔ βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’)))
822rexbidv 3220 . . . . . 6 (π‘₯ = 𝑓 β†’ (βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)))
97, 8orbi12d 918 . . . . 5 (π‘₯ = 𝑓 β†’ ((βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£)) ↔ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£))))
101, 9elab 3668 . . . 4 (𝑓 ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} ↔ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)))
11 gonar 34375 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)))
12 elndif 4128 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
1312adantr 482 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
1413intnanrd 491 . . . . . . . . . . . . . . 15 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)))
1511, 14syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)))
1615ex 414 . . . . . . . . . . . . 13 (𝑁 ∈ Ο‰ β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁))))
1716con2d 134 . . . . . . . . . . . 12 (𝑁 ∈ Ο‰ β†’ ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
1817impl 457 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘))
19 elneeldif 3962 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ (Fmlaβ€˜π‘) ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ π‘Ž β‰  𝑒)
2019necomd 2997 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ (Fmlaβ€˜π‘) ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑒 β‰  π‘Ž)
2120ancoms 460 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ 𝑒 β‰  π‘Ž)
2221neneqd 2946 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 = π‘Ž)
2322orcd 872 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
24 ianor 981 . . . . . . . . . . . . . . . . . . . 20 (Β¬ (𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ↔ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
25 vex 3479 . . . . . . . . . . . . . . . . . . . . 21 𝑒 ∈ V
26 vex 3479 . . . . . . . . . . . . . . . . . . . . 21 𝑣 ∈ V
2725, 26opth 5476 . . . . . . . . . . . . . . . . . . . 20 (βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ© ↔ (𝑒 = π‘Ž ∧ 𝑣 = 𝑏))
2824, 27xchnxbir 333 . . . . . . . . . . . . . . . . . . 19 (Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ© ↔ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
2923, 28sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©)
3029olcd 873 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
31 ianor 981 . . . . . . . . . . . . . . . . . 18 (Β¬ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©) ↔ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
32 gonafv 34330 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ V ∧ 𝑣 ∈ V) β†’ (π‘’βŠΌπ‘”π‘£) = ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ©)
3332el2v 3483 . . . . . . . . . . . . . . . . . . . 20 (π‘’βŠΌπ‘”π‘£) = ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ©
34 gonafv 34330 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ V ∧ 𝑏 ∈ V) β†’ (π‘ŽβŠΌπ‘”π‘) = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©)
3534el2v 3483 . . . . . . . . . . . . . . . . . . . 20 (π‘ŽβŠΌπ‘”π‘) = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©
3633, 35eqeq12i 2751 . . . . . . . . . . . . . . . . . . 19 ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ© = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©)
37 1oex 8473 . . . . . . . . . . . . . . . . . . . 20 1o ∈ V
38 opex 5464 . . . . . . . . . . . . . . . . . . . 20 βŸ¨π‘’, π‘£βŸ© ∈ V
3937, 38opth 5476 . . . . . . . . . . . . . . . . . . 19 (⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ© = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ© ↔ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
4036, 39bitri 275 . . . . . . . . . . . . . . . . . 18 ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
4131, 40xchnxbir 333 . . . . . . . . . . . . . . . . 17 (Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
4230, 41sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4342ralrimivw 3151 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4443ralrimiva 3147 . . . . . . . . . . . . . 14 (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4544adantl 483 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4645adantr 482 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
47 gonanegoal 34332 . . . . . . . . . . . . . . . 16 (π‘’βŠΌπ‘”π‘£) β‰  βˆ€π‘”π‘—π‘Ž
4847neii 2943 . . . . . . . . . . . . . . 15 Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž
4948a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
5049ralrimivw 3151 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
5150ralrimivw 3151 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
52 r19.26 3112 . . . . . . . . . . . 12 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
5346, 51, 52sylanbrc 584 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
5418, 53jca 513 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
55 eleq1 2822 . . . . . . . . . . . 12 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 ∈ (Fmlaβ€˜π‘) ↔ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
5655notbid 318 . . . . . . . . . . 11 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ↔ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
57 eqeq1 2737 . . . . . . . . . . . . . . 15 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
5857notbid 318 . . . . . . . . . . . . . 14 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
5958ralbidv 3178 . . . . . . . . . . . . 13 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
60 eqeq1 2737 . . . . . . . . . . . . . . 15 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 = βˆ€π‘”π‘—π‘Ž ↔ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6160notbid 318 . . . . . . . . . . . . . 14 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6261ralbidv 3178 . . . . . . . . . . . . 13 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6359, 62anbi12d 632 . . . . . . . . . . . 12 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
6463ralbidv 3178 . . . . . . . . . . 11 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
6556, 64anbi12d 632 . . . . . . . . . 10 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))))
6654, 65syl5ibrcom 246 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
6766rexlimdva 3156 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
68 goalr 34377 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)) β†’ 𝑒 ∈ (Fmlaβ€˜π‘))
6968, 12syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
7069ex 414 . . . . . . . . . . . . . 14 (𝑁 ∈ Ο‰ β†’ (βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
7170con2d 134 . . . . . . . . . . . . 13 (𝑁 ∈ Ο‰ β†’ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)))
7271imp 408 . . . . . . . . . . . 12 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘))
7372adantr 482 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘))
74 gonanegoal 34332 . . . . . . . . . . . . . . . 16 (π‘ŽβŠΌπ‘”π‘) β‰  βˆ€π‘”π‘–π‘’
7574nesymi 2999 . . . . . . . . . . . . . . 15 Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘)
7675a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7776ralrimivw 3151 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7877ralrimivw 3151 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7922olcd 873 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
80 ianor 981 . . . . . . . . . . . . . . . . . . . 20 (Β¬ (𝑖 = 𝑗 ∧ 𝑒 = π‘Ž) ↔ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
81 vex 3479 . . . . . . . . . . . . . . . . . . . . 21 𝑖 ∈ V
8281, 25opth 5476 . . . . . . . . . . . . . . . . . . . 20 (βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ© ↔ (𝑖 = 𝑗 ∧ 𝑒 = π‘Ž))
8380, 82xchnxbir 333 . . . . . . . . . . . . . . . . . . 19 (Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ© ↔ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
8479, 83sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©)
8584olcd 873 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
86 ianor 981 . . . . . . . . . . . . . . . . . . 19 (Β¬ (2o = 2o ∧ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©) ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
87 2oex 8474 . . . . . . . . . . . . . . . . . . . 20 2o ∈ V
88 opex 5464 . . . . . . . . . . . . . . . . . . . 20 βŸ¨π‘–, π‘’βŸ© ∈ V
8987, 88opth 5476 . . . . . . . . . . . . . . . . . . 19 (⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ© ↔ (2o = 2o ∧ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
9086, 89xchnxbir 333 . . . . . . . . . . . . . . . . . 18 (Β¬ ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ© ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
91 df-goal 34322 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘”π‘–π‘’ = ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ©
92 df-goal 34322 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘”π‘—π‘Ž = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ©
9391, 92eqeq12i 2751 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ©)
9490, 93xchnxbir 333 . . . . . . . . . . . . . . . . 17 (Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
9585, 94sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9695ralrimivw 3151 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9796ralrimiva 3147 . . . . . . . . . . . . . 14 (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9897adantl 483 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9998adantr 482 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
100 r19.26 3112 . . . . . . . . . . . 12 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž))
10178, 99, 100sylanbrc 584 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž))
10273, 101jca 513 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ (Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)))
103 eleq1 2822 . . . . . . . . . . . . 13 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ↔ 𝑓 ∈ (Fmlaβ€˜π‘)))
104103notbid 318 . . . . . . . . . . . 12 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ↔ Β¬ 𝑓 ∈ (Fmlaβ€˜π‘)))
105 eqeq1 2737 . . . . . . . . . . . . . . . 16 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
106105notbid 318 . . . . . . . . . . . . . . 15 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
107106ralbidv 3178 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
108 eqeq1 2737 . . . . . . . . . . . . . . . 16 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ 𝑓 = βˆ€π‘”π‘—π‘Ž))
109108notbid 318 . . . . . . . . . . . . . . 15 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
110109ralbidv 3178 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
111107, 110anbi12d 632 . . . . . . . . . . . . 13 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
112111ralbidv 3178 . . . . . . . . . . . 12 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
113104, 112anbi12d 632 . . . . . . . . . . 11 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ ((Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
114113eqcoms 2741 . . . . . . . . . 10 (𝑓 = βˆ€π‘”π‘–π‘’ β†’ ((Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
115102, 114syl5ibcom 244 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ (𝑓 = βˆ€π‘”π‘–π‘’ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
116115rexlimdva 3156 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
11767, 116jaod 858 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ ((βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
118117rexlimdva 3156 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
119 elndif 4128 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
120119adantl 483 . . . . . . . . . . . . . . 15 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
121120intnand 490 . . . . . . . . . . . . . 14 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
12211, 121syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
123122ex 414 . . . . . . . . . . . 12 (𝑁 ∈ Ο‰ β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))))
124123con2d 134 . . . . . . . . . . 11 (𝑁 ∈ Ο‰ β†’ ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
125124impl 457 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘))
126 elneeldif 3962 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑏 β‰  𝑣)
127126necomd 2997 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑣 β‰  𝑏)
128127ancoms 460 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ 𝑣 β‰  𝑏)
129128neneqd 2946 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑣 = 𝑏)
130129olcd 873 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
131130, 28sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©)
132131intnand 490 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
133132, 40sylnibr 329 . . . . . . . . . . . . . 14 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
134133ralrimiva 3147 . . . . . . . . . . . . 13 (𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
135134ralrimivw 3151 . . . . . . . . . . . 12 (𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
136135adantl 483 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
13748a1i 11 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
138137ralrimivw 3151 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
139138ralrimivw 3151 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
140136, 139, 52sylanbrc 584 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
141125, 140jca 513 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
142 eleq1 2822 . . . . . . . . . . . 12 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ↔ 𝑓 ∈ (Fmlaβ€˜π‘)))
143142notbid 318 . . . . . . . . . . 11 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ↔ Β¬ 𝑓 ∈ (Fmlaβ€˜π‘)))
144 eqeq1 2737 . . . . . . . . . . . . . . 15 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
145144notbid 318 . . . . . . . . . . . . . 14 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
146145ralbidv 3178 . . . . . . . . . . . . 13 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
147 eqeq1 2737 . . . . . . . . . . . . . . 15 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ 𝑓 = βˆ€π‘”π‘—π‘Ž))
148147notbid 318 . . . . . . . . . . . . . 14 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
149148ralbidv 3178 . . . . . . . . . . . . 13 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
150146, 149anbi12d 632 . . . . . . . . . . . 12 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
151150ralbidv 3178 . . . . . . . . . . 11 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
152143, 151anbi12d 632 . . . . . . . . . 10 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
153152eqcoms 2741 . . . . . . . . 9 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
154141, 153syl5ibcom 244 . . . . . . . 8 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
155154rexlimdva 3156 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) β†’ (βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
156155rexlimdva 3156 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
157118, 156jaod 858 . . . . 5 (𝑁 ∈ Ο‰ β†’ ((βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
158 isfmlasuc 34368 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑓 ∈ V) β†’ (𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
159158elvd 3482 . . . . . . 7 (𝑁 ∈ Ο‰ β†’ (𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
160159notbid 318 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
161 ioran 983 . . . . . . 7 (Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
162 ralnex 3073 . . . . . . . . . . . 12 (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘))
163 ralnex 3073 . . . . . . . . . . . 12 (βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)
164162, 163anbi12i 628 . . . . . . . . . . 11 ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
165 ioran 983 . . . . . . . . . . 11 (Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
166164, 165bitr4i 278 . . . . . . . . . 10 ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
167166ralbii 3094 . . . . . . . . 9 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘) Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
168 ralnex 3073 . . . . . . . . 9 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘) Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
169167, 168bitr2i 276 . . . . . . . 8 (Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
170169anbi2i 624 . . . . . . 7 ((Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
171161, 170bitri 275 . . . . . 6 (Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
172160, 171bitrdi 287 . . . . 5 (𝑁 ∈ Ο‰ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
173157, 172sylibrd 259 . . . 4 (𝑁 ∈ Ο‰ β†’ ((βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)) β†’ Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁)))
17410, 173biimtrid 241 . . 3 (𝑁 ∈ Ο‰ β†’ (𝑓 ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} β†’ Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁)))
175174ralrimiv 3146 . 2 (𝑁 ∈ Ο‰ β†’ βˆ€π‘“ ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁))
176 disjr 4449 . 2 (((Fmlaβ€˜suc 𝑁) ∩ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))}) = βˆ… ↔ βˆ€π‘“ ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁))
177175, 176sylibr 233 1 (𝑁 ∈ Ο‰ β†’ ((Fmlaβ€˜suc 𝑁) ∩ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))}) = βˆ…)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆ– cdif 3945   ∩ cin 3947  βˆ…c0 4322  βŸ¨cop 4634  suc csuc 6364  β€˜cfv 6541  (class class class)co 7406  Ο‰com 7852  1oc1o 8456  2oc2o 8457  βŠΌπ‘”cgna 34314  βˆ€π‘”cgol 34315  Fmlacfmla 34317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  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 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-map 8819  df-goel 34320  df-gona 34321  df-goal 34322  df-sat 34323  df-fmla 34325
This theorem is referenced by:  satffunlem2lem2  34386
  Copyright terms: Public domain W3C validator