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 34688
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 3476 . . . . 5 𝑓 ∈ V
2 eqeq1 2734 . . . . . . . . 9 (π‘₯ = 𝑓 β†’ (π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ 𝑓 = (π‘’βŠΌπ‘”π‘£)))
32rexbidv 3176 . . . . . . . 8 (π‘₯ = 𝑓 β†’ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ↔ βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£)))
4 eqeq1 2734 . . . . . . . . 9 (π‘₯ = 𝑓 β†’ (π‘₯ = βˆ€π‘”π‘–π‘’ ↔ 𝑓 = βˆ€π‘”π‘–π‘’))
54rexbidv 3176 . . . . . . . 8 (π‘₯ = 𝑓 β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’ ↔ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’))
63, 5orbi12d 915 . . . . . . 7 (π‘₯ = 𝑓 β†’ ((βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ↔ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’)))
76rexbidv 3176 . . . . . 6 (π‘₯ = 𝑓 β†’ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ↔ βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’)))
822rexbidv 3217 . . . . . 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 3667 . . . 4 (𝑓 ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} ↔ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)))
11 gonar 34684 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)))
12 elndif 4127 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
1312adantr 479 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
1413intnanrd 488 . . . . . . . . . . . . . . 15 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)))
1511, 14syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)))
1615ex 411 . . . . . . . . . . . . 13 (𝑁 ∈ Ο‰ β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) β†’ Β¬ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁))))
1716con2d 134 . . . . . . . . . . . 12 (𝑁 ∈ Ο‰ β†’ ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
1817impl 454 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘))
19 elneeldif 3961 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ (Fmlaβ€˜π‘) ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ π‘Ž β‰  𝑒)
2019necomd 2994 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ (Fmlaβ€˜π‘) ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑒 β‰  π‘Ž)
2120ancoms 457 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ 𝑒 β‰  π‘Ž)
2221neneqd 2943 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 = π‘Ž)
2322orcd 869 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
24 ianor 978 . . . . . . . . . . . . . . . . . . . 20 (Β¬ (𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ↔ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
25 vex 3476 . . . . . . . . . . . . . . . . . . . . 21 𝑒 ∈ V
26 vex 3476 . . . . . . . . . . . . . . . . . . . . 21 𝑣 ∈ V
2725, 26opth 5475 . . . . . . . . . . . . . . . . . . . 20 (βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ© ↔ (𝑒 = π‘Ž ∧ 𝑣 = 𝑏))
2824, 27xchnxbir 332 . . . . . . . . . . . . . . . . . . 19 (Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ© ↔ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
2923, 28sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©)
3029olcd 870 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
31 ianor 978 . . . . . . . . . . . . . . . . . 18 (Β¬ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©) ↔ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
32 gonafv 34639 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ V ∧ 𝑣 ∈ V) β†’ (π‘’βŠΌπ‘”π‘£) = ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ©)
3332el2v 3480 . . . . . . . . . . . . . . . . . . . 20 (π‘’βŠΌπ‘”π‘£) = ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ©
34 gonafv 34639 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ V ∧ 𝑏 ∈ V) β†’ (π‘ŽβŠΌπ‘”π‘) = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©)
3534el2v 3480 . . . . . . . . . . . . . . . . . . . 20 (π‘ŽβŠΌπ‘”π‘) = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©
3633, 35eqeq12i 2748 . . . . . . . . . . . . . . . . . . 19 ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ ⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ© = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ©)
37 1oex 8478 . . . . . . . . . . . . . . . . . . . 20 1o ∈ V
38 opex 5463 . . . . . . . . . . . . . . . . . . . 20 βŸ¨π‘’, π‘£βŸ© ∈ V
3937, 38opth 5475 . . . . . . . . . . . . . . . . . . 19 (⟨1o, βŸ¨π‘’, π‘£βŸ©βŸ© = ⟨1o, βŸ¨π‘Ž, π‘βŸ©βŸ© ↔ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
4036, 39bitri 274 . . . . . . . . . . . . . . . . . 18 ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
4131, 40xchnxbir 332 . . . . . . . . . . . . . . . . 17 (Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ (Β¬ 1o = 1o ∨ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
4230, 41sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4342ralrimivw 3148 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4443ralrimiva 3144 . . . . . . . . . . . . . 14 (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4544adantl 480 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
4645adantr 479 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
47 gonanegoal 34641 . . . . . . . . . . . . . . . 16 (π‘’βŠΌπ‘”π‘£) β‰  βˆ€π‘”π‘—π‘Ž
4847neii 2940 . . . . . . . . . . . . . . 15 Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž
4948a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
5049ralrimivw 3148 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
5150ralrimivw 3148 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
52 r19.26 3109 . . . . . . . . . . . 12 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
5346, 51, 52sylanbrc 581 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
5418, 53jca 510 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
55 eleq1 2819 . . . . . . . . . . . 12 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 ∈ (Fmlaβ€˜π‘) ↔ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
5655notbid 317 . . . . . . . . . . 11 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ↔ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
57 eqeq1 2734 . . . . . . . . . . . . . . 15 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
5857notbid 317 . . . . . . . . . . . . . 14 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
5958ralbidv 3175 . . . . . . . . . . . . 13 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘)))
60 eqeq1 2734 . . . . . . . . . . . . . . 15 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (𝑓 = βˆ€π‘”π‘—π‘Ž ↔ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6160notbid 317 . . . . . . . . . . . . . 14 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6261ralbidv 3175 . . . . . . . . . . . . 13 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
6359, 62anbi12d 629 . . . . . . . . . . . 12 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
6463ralbidv 3175 . . . . . . . . . . 11 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
6556, 64anbi12d 629 . . . . . . . . . 10 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))))
6654, 65syl5ibrcom 246 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑣 ∈ (Fmlaβ€˜suc 𝑁)) β†’ (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
6766rexlimdva 3153 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
68 goalr 34686 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)) β†’ 𝑒 ∈ (Fmlaβ€˜π‘))
6968, 12syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Ο‰ ∧ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
7069ex 411 . . . . . . . . . . . . . 14 (𝑁 ∈ Ο‰ β†’ (βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
7170con2d 134 . . . . . . . . . . . . 13 (𝑁 ∈ Ο‰ β†’ (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘)))
7271imp 405 . . . . . . . . . . . 12 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘))
7372adantr 479 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘))
74 gonanegoal 34641 . . . . . . . . . . . . . . . 16 (π‘ŽβŠΌπ‘”π‘) β‰  βˆ€π‘”π‘–π‘’
7574nesymi 2996 . . . . . . . . . . . . . . 15 Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘)
7675a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7776ralrimivw 3148 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7877ralrimivw 3148 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘))
7922olcd 870 . . . . . . . . . . . . . . . . . . 19 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
80 ianor 978 . . . . . . . . . . . . . . . . . . . 20 (Β¬ (𝑖 = 𝑗 ∧ 𝑒 = π‘Ž) ↔ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
81 vex 3476 . . . . . . . . . . . . . . . . . . . . 21 𝑖 ∈ V
8281, 25opth 5475 . . . . . . . . . . . . . . . . . . . 20 (βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ© ↔ (𝑖 = 𝑗 ∧ 𝑒 = π‘Ž))
8380, 82xchnxbir 332 . . . . . . . . . . . . . . . . . . 19 (Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ© ↔ (Β¬ 𝑖 = 𝑗 ∨ Β¬ 𝑒 = π‘Ž))
8479, 83sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©)
8584olcd 870 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
86 ianor 978 . . . . . . . . . . . . . . . . . . 19 (Β¬ (2o = 2o ∧ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©) ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
87 2oex 8479 . . . . . . . . . . . . . . . . . . . 20 2o ∈ V
88 opex 5463 . . . . . . . . . . . . . . . . . . . 20 βŸ¨π‘–, π‘’βŸ© ∈ V
8987, 88opth 5475 . . . . . . . . . . . . . . . . . . 19 (⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ© ↔ (2o = 2o ∧ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
9086, 89xchnxbir 332 . . . . . . . . . . . . . . . . . 18 (Β¬ ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ© ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
91 df-goal 34631 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘”π‘–π‘’ = ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ©
92 df-goal 34631 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘”π‘—π‘Ž = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ©
9391, 92eqeq12i 2748 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ ⟨2o, βŸ¨π‘–, π‘’βŸ©βŸ© = ⟨2o, βŸ¨π‘—, π‘ŽβŸ©βŸ©)
9490, 93xchnxbir 332 . . . . . . . . . . . . . . . . 17 (Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ (Β¬ 2o = 2o ∨ Β¬ βŸ¨π‘–, π‘’βŸ© = βŸ¨π‘—, π‘ŽβŸ©))
9585, 94sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9695ralrimivw 3148 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ π‘Ž ∈ (Fmlaβ€˜π‘)) β†’ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9796ralrimiva 3144 . . . . . . . . . . . . . 14 (𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9897adantl 480 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
9998adantr 479 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)
100 r19.26 3109 . . . . . . . . . . . 12 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž))
10178, 99, 100sylanbrc 581 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž))
10273, 101jca 510 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ (Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)))
103 eleq1 2819 . . . . . . . . . . . . 13 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ↔ 𝑓 ∈ (Fmlaβ€˜π‘)))
104103notbid 317 . . . . . . . . . . . 12 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ↔ Β¬ 𝑓 ∈ (Fmlaβ€˜π‘)))
105 eqeq1 2734 . . . . . . . . . . . . . . . 16 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
106105notbid 317 . . . . . . . . . . . . . . 15 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
107106ralbidv 3175 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
108 eqeq1 2734 . . . . . . . . . . . . . . . 16 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ 𝑓 = βˆ€π‘”π‘—π‘Ž))
109108notbid 317 . . . . . . . . . . . . . . 15 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
110109ralbidv 3175 . . . . . . . . . . . . . 14 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
111107, 110anbi12d 629 . . . . . . . . . . . . 13 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
112111ralbidv 3175 . . . . . . . . . . . 12 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
113104, 112anbi12d 629 . . . . . . . . . . 11 (βˆ€π‘”π‘–π‘’ = 𝑓 β†’ ((Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
114113eqcoms 2738 . . . . . . . . . 10 (𝑓 = βˆ€π‘”π‘–π‘’ β†’ ((Β¬ βˆ€π‘”π‘–π‘’ ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ βˆ€π‘”π‘–π‘’ = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ βˆ€π‘”π‘–π‘’ = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
115102, 114syl5ibcom 244 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) ∧ 𝑖 ∈ Ο‰) β†’ (𝑓 = βˆ€π‘”π‘–π‘’ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
116115rexlimdva 3153 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
11767, 116jaod 855 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ ((βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
118117rexlimdva 3153 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
119 elndif 4127 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (Fmlaβ€˜π‘) β†’ Β¬ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
120119adantl 480 . . . . . . . . . . . . . . 15 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
121120intnand 487 . . . . . . . . . . . . . 14 ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
12211, 121syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ Ο‰ ∧ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
123122ex 411 . . . . . . . . . . . 12 (𝑁 ∈ Ο‰ β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) β†’ Β¬ (𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))))
124123con2d 134 . . . . . . . . . . 11 (𝑁 ∈ Ο‰ β†’ ((𝑒 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘)))
125124impl 454 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘))
126 elneeldif 3961 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑏 β‰  𝑣)
127126necomd 2994 . . . . . . . . . . . . . . . . . . . 20 ((𝑏 ∈ (Fmlaβ€˜π‘) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ 𝑣 β‰  𝑏)
128127ancoms 457 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ 𝑣 β‰  𝑏)
129128neneqd 2943 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ 𝑣 = 𝑏)
130129olcd 870 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ (Β¬ 𝑒 = π‘Ž ∨ Β¬ 𝑣 = 𝑏))
131130, 28sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©)
132131intnand 487 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (1o = 1o ∧ βŸ¨π‘’, π‘£βŸ© = βŸ¨π‘Ž, π‘βŸ©))
133132, 40sylnibr 328 . . . . . . . . . . . . . 14 ((𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ∧ 𝑏 ∈ (Fmlaβ€˜π‘)) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
134133ralrimiva 3144 . . . . . . . . . . . . 13 (𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
135134ralrimivw 3148 . . . . . . . . . . . 12 (𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
136135adantl 480 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘))
13748a1i 11 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
138137ralrimivw 3148 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
139138ralrimivw 3148 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)
140136, 139, 52sylanbrc 581 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž))
141125, 140jca 510 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)))
142 eleq1 2819 . . . . . . . . . . . 12 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ↔ 𝑓 ∈ (Fmlaβ€˜π‘)))
143142notbid 317 . . . . . . . . . . 11 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ↔ Β¬ 𝑓 ∈ (Fmlaβ€˜π‘)))
144 eqeq1 2734 . . . . . . . . . . . . . . 15 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
145144notbid 317 . . . . . . . . . . . . . 14 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
146145ralbidv 3175 . . . . . . . . . . . . 13 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ↔ βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘)))
147 eqeq1 2734 . . . . . . . . . . . . . . 15 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ 𝑓 = βˆ€π‘”π‘—π‘Ž))
148147notbid 317 . . . . . . . . . . . . . 14 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
149148ralbidv 3175 . . . . . . . . . . . . 13 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž ↔ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
150146, 149anbi12d 629 . . . . . . . . . . . 12 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
151150ralbidv 3175 . . . . . . . . . . 11 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
152143, 151anbi12d 629 . . . . . . . . . 10 ((π‘’βŠΌπ‘”π‘£) = 𝑓 β†’ ((Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
153152eqcoms 2738 . . . . . . . . 9 (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ ((Β¬ (π‘’βŠΌπ‘”π‘£) ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ (π‘’βŠΌπ‘”π‘£) = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ (π‘’βŠΌπ‘”π‘£) = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
154141, 153syl5ibcom 244 . . . . . . . 8 (((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) ∧ 𝑣 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))) β†’ (𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
155154rexlimdva 3153 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ 𝑒 ∈ (Fmlaβ€˜π‘)) β†’ (βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
156155rexlimdva 3153 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
157118, 156jaod 855 . . . . 5 (𝑁 ∈ Ο‰ β†’ ((βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)𝑓 = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ 𝑓 = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))𝑓 = (π‘’βŠΌπ‘”π‘£)) β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
158 isfmlasuc 34677 . . . . . . . 8 ((𝑁 ∈ Ο‰ ∧ 𝑓 ∈ V) β†’ (𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
159158elvd 3479 . . . . . . 7 (𝑁 ∈ Ο‰ β†’ (𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
160159notbid 317 . . . . . 6 (𝑁 ∈ Ο‰ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
161 ioran 980 . . . . . . 7 (Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
162 ralnex 3070 . . . . . . . . . . . 12 (βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ↔ Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘))
163 ralnex 3070 . . . . . . . . . . . 12 (βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž ↔ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)
164162, 163anbi12i 625 . . . . . . . . . . 11 ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
165 ioran 980 . . . . . . . . . . 11 (Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ (Β¬ βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ Β¬ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
166164, 165bitr4i 277 . . . . . . . . . 10 ((βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
167166ralbii 3091 . . . . . . . . 9 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘) Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
168 ralnex 3070 . . . . . . . . 9 (βˆ€π‘Ž ∈ (Fmlaβ€˜π‘) Β¬ (βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž))
169167, 168bitr2i 275 . . . . . . . 8 (Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž) ↔ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))
170169anbi2i 621 . . . . . . 7 ((Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ Β¬ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
171161, 170bitri 274 . . . . . 6 (Β¬ (𝑓 ∈ (Fmlaβ€˜π‘) ∨ βˆƒπ‘Ž ∈ (Fmlaβ€˜π‘)(βˆƒπ‘ ∈ (Fmlaβ€˜π‘)𝑓 = (π‘ŽβŠΌπ‘”π‘) ∨ βˆƒπ‘— ∈ Ο‰ 𝑓 = βˆ€π‘”π‘—π‘Ž)) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž)))
172160, 171bitrdi 286 . . . . 5 (𝑁 ∈ Ο‰ β†’ (Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁) ↔ (Β¬ 𝑓 ∈ (Fmlaβ€˜π‘) ∧ βˆ€π‘Ž ∈ (Fmlaβ€˜π‘)(βˆ€π‘ ∈ (Fmlaβ€˜π‘) Β¬ 𝑓 = (π‘ŽβŠΌπ‘”π‘) ∧ βˆ€π‘— ∈ Ο‰ Β¬ 𝑓 = βˆ€π‘”π‘—π‘Ž))))
173157, 172sylibrd 258 . . . 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 3143 . 2 (𝑁 ∈ Ο‰ β†’ βˆ€π‘“ ∈ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘£ ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘’βŠΌπ‘”π‘£) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘’) ∨ βˆƒπ‘’ ∈ (Fmlaβ€˜π‘)βˆƒπ‘£ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘’βŠΌπ‘”π‘£))} Β¬ 𝑓 ∈ (Fmlaβ€˜suc 𝑁))
176 disjr 4448 . 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 394   ∨ wo 843   = wceq 1539   ∈ wcel 2104  {cab 2707   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944   ∩ cin 3946  βˆ…c0 4321  βŸ¨cop 4633  suc csuc 6365  β€˜cfv 6542  (class class class)co 7411  Ο‰com 7857  1oc1o 8461  2oc2o 8462  βŠΌπ‘”cgna 34623  βˆ€π‘”cgol 34624  Fmlacfmla 34626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-map 8824  df-goel 34629  df-gona 34630  df-goal 34631  df-sat 34632  df-fmla 34634
This theorem is referenced by:  satffunlem2lem2  34695
  Copyright terms: Public domain W3C validator