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 34879
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 3470 . . . . 5 𝑓 ∈ V
2 eqeq1 2728 . . . . . . . . 9 (π‘₯ = 𝑓 β†’ (π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ 𝑓 = (π‘’βŠΌπ‘”π‘£)))
32rexbidv 3170 . . . . . . . 8 (π‘₯ = 𝑓 β†’ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£)))
4 eqeq1 2728 . . . . . . . . 9 (π‘₯ = 𝑓 β†’ (π‘₯ = βˆ€π‘”π‘–π‘’ ↔ 𝑓 = βˆ€π‘”π‘–π‘’))
54rexbidv 3170 . . . . . . . 8 (π‘₯ = 𝑓 β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’ ↔ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’))
63, 5orbi12d 915 . . . . . . 7 (π‘₯ = 𝑓 β†’ ((βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ↔ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’)))
76rexbidv 3170 . . . . . 6 (π‘₯ = 𝑓 β†’ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ↔ βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’)))
822rexbidv 3211 . . . . . 6 (π‘₯ = 𝑓 β†’ (βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)))
97, 8orbi12d 915 . . . . 5 (π‘₯ = 𝑓 β†’ ((βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£)) ↔ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£))))
101, 9elab 3660 . . . 4 (𝑓 ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} ↔ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)))
11 gonar 34875 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)))
12 elndif 4120 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
1312adantr 480 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
1413intnanrd 489 . . . . . . . . . . . . . . 15 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)))
1511, 14syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)))
1615ex 412 . . . . . . . . . . . . 13 (𝑁 ∈ Ο‰ β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁))))
1716con2d 134 . . . . . . . . . . . 12 (𝑁 ∈ Ο‰ β†’ ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
1817impl 455 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘))
19 elneeldif 3954 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ (Fmlaβ€˜π‘) ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ π‘Ž β‰  𝑒)
2019necomd 2988 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ (Fmlaβ€˜π‘) ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑒 β‰  π‘Ž)
2120ancoms 458 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ 𝑒 β‰  π‘Ž)
2221neneqd 2937 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 = π‘Ž)
2322orcd 870 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
24 ianor 978 . . . . . . . . . . . . . . . . . . . 20 (Β¬ (𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ↔ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
25 vex 3470 . . . . . . . . . . . . . . . . . . . . 21 𝑒 ∈ V
26 vex 3470 . . . . . . . . . . . . . . . . . . . . 21 𝑣 ∈ V
2725, 26opth 5466 . . . . . . . . . . . . . . . . . . . 20 (βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ© ↔ (𝑒 = π‘Ž ∧ 𝑣 = 𝑏))
2824, 27xchnxbir 333 . . . . . . . . . . . . . . . . . . 19 (Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ© ↔ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
2923, 28sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©)
3029olcd 871 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
31 ianor 978 . . . . . . . . . . . . . . . . . 18 (Β¬ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©) ↔ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
32 gonafv 34830 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ V ∧ 𝑣 ∈ V) β†’ (π‘’βŠΌπ‘”π‘£) = ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ©)
3332el2v 3474 . . . . . . . . . . . . . . . . . . . 20 (π‘’βŠΌπ‘”π‘£) = ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ©
34 gonafv 34830 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ V ∧ 𝑏 ∈ V) β†’ (π‘ŽβŠΌπ‘”π‘) = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©)
3534el2v 3474 . . . . . . . . . . . . . . . . . . . 20 (π‘ŽβŠΌπ‘”π‘) = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©
3633, 35eqeq12i 2742 . . . . . . . . . . . . . . . . . . 19 ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ© = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©)
37 1oex 8471 . . . . . . . . . . . . . . . . . . . 20 1o ∈ V
38 opex 5454 . . . . . . . . . . . . . . . . . . . 20 βŸ¨π‘’, π‘£βŸ© ∈ V
3937, 38opth 5466 . . . . . . . . . . . . . . . . . . 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 3142 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4443ralrimiva 3138 . . . . . . . . . . . . . 14 (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4544adantl 481 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4645adantr 480 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
47 gonanegoal 34832 . . . . . . . . . . . . . . . 16 (π‘’βŠΌπ‘”π‘£) β‰  βˆ€π‘”π‘—π‘Ž
4847neii 2934 . . . . . . . . . . . . . . 15 Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž
4948a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
5049ralrimivw 3142 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
5150ralrimivw 3142 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
52 r19.26 3103 . . . . . . . . . . . 12 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
5346, 51, 52sylanbrc 582 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
5418, 53jca 511 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
55 eleq1 2813 . . . . . . . . . . . 12 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 ∈ (Fmlaβ€˜π‘) ↔ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
5655notbid 318 . . . . . . . . . . 11 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ↔ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
57 eqeq1 2728 . . . . . . . . . . . . . . 15 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
5857notbid 318 . . . . . . . . . . . . . 14 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
5958ralbidv 3169 . . . . . . . . . . . . 13 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
60 eqeq1 2728 . . . . . . . . . . . . . . 15 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 = βˆ€π‘”π‘—π‘Ž ↔ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6160notbid 318 . . . . . . . . . . . . . 14 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6261ralbidv 3169 . . . . . . . . . . . . 13 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6359, 62anbi12d 630 . . . . . . . . . . . 12 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
6463ralbidv 3169 . . . . . . . . . . 11 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
6556, 64anbi12d 630 . . . . . . . . . 10 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))))
6654, 65syl5ibrcom 246 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
6766rexlimdva 3147 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
68 goalr 34877 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)) β†’ 𝑒 ∈ (Fmlaβ€˜π‘))
6968, 12syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
7069ex 412 . . . . . . . . . . . . . 14 (𝑁 ∈ Ο‰ β†’ (βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
7170con2d 134 . . . . . . . . . . . . 13 (𝑁 ∈ Ο‰ β†’ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)))
7271imp 406 . . . . . . . . . . . 12 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘))
7372adantr 480 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘))
74 gonanegoal 34832 . . . . . . . . . . . . . . . 16 (π‘ŽβŠΌπ‘”π‘) β‰  βˆ€π‘”π‘–π‘’
7574nesymi 2990 . . . . . . . . . . . . . . 15 Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘)
7675a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7776ralrimivw 3142 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7877ralrimivw 3142 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7922olcd 871 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
80 ianor 978 . . . . . . . . . . . . . . . . . . . 20 (Β¬ (𝑖 = 𝑗 ∧ 𝑒 = π‘Ž) ↔ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
81 vex 3470 . . . . . . . . . . . . . . . . . . . . 21 𝑖 ∈ V
8281, 25opth 5466 . . . . . . . . . . . . . . . . . . . 20 (βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ© ↔ (𝑖 = 𝑗 ∧ 𝑒 = π‘Ž))
8380, 82xchnxbir 333 . . . . . . . . . . . . . . . . . . 19 (Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ© ↔ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
8479, 83sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©)
8584olcd 871 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
86 ianor 978 . . . . . . . . . . . . . . . . . . 19 (Β¬ (2o = 2o ∧ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©) ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
87 2oex 8472 . . . . . . . . . . . . . . . . . . . 20 2o ∈ V
88 opex 5454 . . . . . . . . . . . . . . . . . . . 20 βŸ¨π‘–, π‘’βŸ© ∈ V
8987, 88opth 5466 . . . . . . . . . . . . . . . . . . 19 (⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ© ↔ (2o = 2o ∧ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
9086, 89xchnxbir 333 . . . . . . . . . . . . . . . . . 18 (Β¬ ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ© ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
91 df-goal 34822 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘”π‘–π‘’ = ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ©
92 df-goal 34822 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘”π‘—π‘Ž = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ©
9391, 92eqeq12i 2742 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ©)
9490, 93xchnxbir 333 . . . . . . . . . . . . . . . . 17 (Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
9585, 94sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9695ralrimivw 3142 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9796ralrimiva 3138 . . . . . . . . . . . . . 14 (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9897adantl 481 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9998adantr 480 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
100 r19.26 3103 . . . . . . . . . . . 12 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž))
10178, 99, 100sylanbrc 582 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž))
10273, 101jca 511 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ (Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)))
103 eleq1 2813 . . . . . . . . . . . . 13 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ↔ 𝑓 ∈ (Fmlaβ€˜π‘)))
104103notbid 318 . . . . . . . . . . . 12 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ↔ Β¬ 𝑓 ∈ (Fmlaβ€˜π‘)))
105 eqeq1 2728 . . . . . . . . . . . . . . . 16 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
106105notbid 318 . . . . . . . . . . . . . . 15 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
107106ralbidv 3169 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
108 eqeq1 2728 . . . . . . . . . . . . . . . 16 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ 𝑓 = βˆ€π‘”π‘—π‘Ž))
109108notbid 318 . . . . . . . . . . . . . . 15 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
110109ralbidv 3169 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
111107, 110anbi12d 630 . . . . . . . . . . . . 13 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
112111ralbidv 3169 . . . . . . . . . . . 12 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
113104, 112anbi12d 630 . . . . . . . . . . 11 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ ((Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
114113eqcoms 2732 . . . . . . . . . 10 (𝑓 = βˆ€π‘”π‘–π‘’ β†’ ((Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
115102, 114syl5ibcom 244 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ (𝑓 = βˆ€π‘”π‘–π‘’ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
116115rexlimdva 3147 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
11767, 116jaod 856 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ ((βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
118117rexlimdva 3147 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
119 elndif 4120 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
120119adantl 481 . . . . . . . . . . . . . . 15 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
121120intnand 488 . . . . . . . . . . . . . 14 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
12211, 121syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
123122ex 412 . . . . . . . . . . . 12 (𝑁 ∈ Ο‰ β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))))
124123con2d 134 . . . . . . . . . . 11 (𝑁 ∈ Ο‰ β†’ ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
125124impl 455 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘))
126 elneeldif 3954 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑏 β‰  𝑣)
127126necomd 2988 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑣 β‰  𝑏)
128127ancoms 458 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ 𝑣 β‰  𝑏)
129128neneqd 2937 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑣 = 𝑏)
130129olcd 871 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
131130, 28sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©)
132131intnand 488 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
133132, 40sylnibr 329 . . . . . . . . . . . . . 14 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
134133ralrimiva 3138 . . . . . . . . . . . . 13 (𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
135134ralrimivw 3142 . . . . . . . . . . . 12 (𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
136135adantl 481 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
13748a1i 11 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
138137ralrimivw 3142 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
139138ralrimivw 3142 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
140136, 139, 52sylanbrc 582 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
141125, 140jca 511 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
142 eleq1 2813 . . . . . . . . . . . 12 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ↔ 𝑓 ∈ (Fmlaβ€˜π‘)))
143142notbid 318 . . . . . . . . . . 11 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ↔ Β¬ 𝑓 ∈ (Fmlaβ€˜π‘)))
144 eqeq1 2728 . . . . . . . . . . . . . . 15 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
145144notbid 318 . . . . . . . . . . . . . 14 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
146145ralbidv 3169 . . . . . . . . . . . . 13 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
147 eqeq1 2728 . . . . . . . . . . . . . . 15 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ 𝑓 = βˆ€π‘”π‘—π‘Ž))
148147notbid 318 . . . . . . . . . . . . . 14 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
149148ralbidv 3169 . . . . . . . . . . . . 13 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
150146, 149anbi12d 630 . . . . . . . . . . . 12 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
151150ralbidv 3169 . . . . . . . . . . 11 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
152143, 151anbi12d 630 . . . . . . . . . 10 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
153152eqcoms 2732 . . . . . . . . 9 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
154141, 153syl5ibcom 244 . . . . . . . 8 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
155154rexlimdva 3147 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) β†’ (βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
156155rexlimdva 3147 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
157118, 156jaod 856 . . . . 5 (𝑁 ∈ Ο‰ β†’ ((βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
158 isfmlasuc 34868 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑓 ∈ V) β†’ (𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
159158elvd 3473 . . . . . . 7 (𝑁 ∈ Ο‰ β†’ (𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
160159notbid 318 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
161 ioran 980 . . . . . . 7 (Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
162 ralnex 3064 . . . . . . . . . . . 12 (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘))
163 ralnex 3064 . . . . . . . . . . . 12 (βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)
164162, 163anbi12i 626 . . . . . . . . . . 11 ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
165 ioran 980 . . . . . . . . . . 11 (Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
166164, 165bitr4i 278 . . . . . . . . . 10 ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
167166ralbii 3085 . . . . . . . . 9 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘) Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
168 ralnex 3064 . . . . . . . . 9 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘) Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
169167, 168bitr2i 276 . . . . . . . 8 (Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
170169anbi2i 622 . . . . . . 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 3137 . 2 (𝑁 ∈ Ο‰ β†’ βˆ€π‘“ ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁))
176 disjr 4441 . 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 395   ∨ wo 844   = wceq 1533   ∈ wcel 2098  {cab 2701   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  Vcvv 3466   βˆ– cdif 3937   ∩ cin 3939  βˆ…c0 4314  βŸ¨cop 4626  suc csuc 6356  β€˜cfv 6533  (class class class)co 7401  Ο‰com 7848  1oc1o 8454  2oc2o 8455  βŠΌπ‘”cgna 34814  βˆ€π‘”cgol 34815  Fmlacfmla 34817
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-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  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-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-map 8818  df-goel 34820  df-gona 34821  df-goal 34822  df-sat 34823  df-fmla 34825
This theorem is referenced by:  satffunlem2lem2  34886
  Copyright terms: Public domain W3C validator